Removed formal/warp-v_formal.tlv, favoring direct use of warp-v.tlv w…

…ith --m4def M4_FORMAL=1.

Improved waterfall VIZ prior to https://www.linkedin.com/posts/steve-hoover-a44b607_formalverification-visualdebug-warpv-ugcPost-6920065393508163587-9kqY
Added riscv-formal reg checker VIZ.

.travis.yml

@@ -24,6 +24,9 @@ before_script:
   - cd formal
   - if ("$TRAVIS_PULL_REQUEST"); then export BUILD_PATH=$TRAVIS_PULL_REQUEST_SLUG; else export BUILD_PATH=$TRAVIS_REPO_SLUG; fi
 
+# TODO : Travis stopped providing free computes.
+# TODO : Changes have been made that would break this, but we need to rework this for a different CI system anyway.
+#        Below refers to .../formal/warp-v_formal.tlv which used to be a top-level file, but now .../warp-v.tlv is used directly.
 # TODO : riscv-formal for 6 stage implementation
 jobs :
   include :

formal/Makefile

@@ -11,11 +11,12 @@ export PATH:=$(shell pwd)/env/bin:$(PATH)
 tos_agree:
 	yes | sandpiper-saas
 
-# Run SandPiper Cloud Edition(TM) (SandPiper(TM) in the cloud for open-source code).
-out/warp-v_formal.sv: warp-v_formal.tlv ../warp-v.tlv
+# Run SandPiper-SaaS(TM).
+out/warp-v_formal.sv: ../warp-v.tlv
 	rm -rf out
 	mkdir out
-	sandpiper-saas -i warp-v_formal.tlv -f ../warp-v.tlv -o warp-v_formal.sv --outdir out --sv_url_inc --iArgs
+	# Note: Currently "--m4def M4_FORMAL=1" only works as the final args due to https://gitlab.com/rweda/sandpiper-saas/-/issues/2
+	sandpiper-saas -i ../warp-v.tlv -o warp-v_formal.sv --outdir out --sv_url_inc --iArgs --debugSigsGtkwave --debugSigsYosys --m4def M4_FORMAL=1
 
 env: env/PASSED
 

formal/README.md

@@ -19,7 +19,7 @@ make verif
 WARP-V uses riscv-formal for formal verification. The script `make_env.sh` (run by the `Makefile`) is provided to
 download and build the necessary tools in the manner described in this <a href="https://github.com/cliffordwolf/riscv-formal/blob/master/docs/quickstart.md" target="_blank" atom_fix="_">QuickStart Guide</a>.
 
-`warp-v_formal.tlv` can be compiled with SandPiper(TM) SaaS Edition (running in the cloud) using:
+`warp-v.tlv` can be compiled with SandPiper(TM) SaaS Edition (running in the cloud) for formal verification using:
 
 ```sh
 make compile

formal/checks.cfg

@@ -10,7 +10,7 @@ insn            29
 reg       15    26
 pc_fwd    10    28
 pc_bwd    10    28
-liveness  1  16 26
+liveness  1  16  35
 unique    1  16 26
 causal    10    28