Enabling use of SandPiper(TM) SaaS Edition and removing pre-commit Sa…

…ndPiper compilation.

.travis.yml

@@ -19,7 +19,7 @@ before_script:
   - cd formal
 script:
   # Run riscv-formal for WARP-V.
-  - PATH=/home/travis/build/stevehoover/warp-v/formal/env/bin:$PATH bash -c 'touch build.sv && make verif'
+  - PATH=/home/travis/build/stevehoover/warp-v/formal/env/bin:$PATH bash -c 'make verif'
 after_success:
 after_failure:
   # Upload files for debug.

README.md

@@ -53,14 +53,16 @@ git submodule update
 
 ### Considerations
 
-Contributions are welcomed. Be aware, however, that WARP-V is probably the worst possible first exposure to TL-Verilog. It utilizes advanced capabilities that are not yet officially supported. If you are new to TL-Verilog, utilize the resources available in Makerchip to learn TL-Verilog in baby steps before jumping into WARP-V.
+Contributions are welcomed. Be aware, however, that WARP-V is probably the worst possible first exposure to TL-Verilog. It utilizes advanced proof-of-concept capabilities that are not officially supported. If you are new to TL-Verilog, utilize the resources available in Makerchip to learn TL-Verilog in baby steps before jumping into WARP-V.
 
 With a clear understanding of where to tread, you can navigate WARP-V and contribute successfully. WARP-V is a library with plenty of room to grow. Be aware, however, that working with CPU microarchitecture means walking in a minefield of patents. Work with the community to define your contributions.
 
 To work with WARP-V without stumbling over the undocumented features it utilizes, it is important to understand the tool stack. TL-Verilog is well-defined with reasonable documentation, examples, and interactive tutorials in Makerchip. It is a mature and extremely compelling tool stack that supports timing-abstract and transaction-level design techniques you cannot find elsewhere. WARP-V goes a step further, utilizing an undocumented proof-of-concept framework that supports advanced features for modularity, reuse, parameterization, and code generation. These features are provided using a macro preprocessor called M4 plus a bit of Perl. Though they can be used in Makerchip, they have no long-term support.
 
 There is a clear distinction between these layers, and Makerchip helps to work with them. If you load WARP-V into Makerchip (using the link above), you'll see the source code in the "Editor" pane, and the pre-processed TL-Verilog code (which you can navigate and debug) in the "Nav-TLV" pane. Clicking line numbers in this pane will take you to the source line that generated it. You can cut and paste from Nat-TLV into the Editor to avoid the preprocessing all together.
 
+formal/Makefile uses SandPiper(TM) SaaS Edition -- SandPiper running in the cloud as a service. No local SandPiper installation is required, but if the service goes down, the build will fail.
+
 ### Workflow
 
 Work in a fork and submit push requests that have passed continuous integration (CI) testing (below). Your work is much more likely to be accepted if it is aligned with the community and doesn't risk patent infringement.
@@ -73,8 +75,6 @@ WARP-V is verified using the <a href="https://github.com/cliffordwolf/riscv-form
 
 <a href="https://travis-ci.com/" target="_blank">Travis-CI</a> is used for continuous integration testing: <a href="https://travis-ci.com/stevehoover/warp-v" target="_blank">WARP-V Travis CI</a>. CI runs formal verification tests.
 
-**`pre-commit`**: Currently, SandPiper is not available for public download due to export restrictions, so it cannot be available in the CI environment. SV sources must be pre-built and included in the repository. Run the `pre-commit` script to run sandpiper locally. This will also configure your local repo to run `pre-commit` as a pre-commit hook in the future.
-
 **CI Environment**: CI uses the `formal/make_env.sh` script to built the necessary tools from source. The result of this build is cached between builds (per branch) using a <a href="https://docs.travis-ci.com/user/caching" target="_blank">caching feature of Travis-CI</a>. Caching is applied blindly, without regard to the availability of newer sources. CI scripts will check the latest sources against the ones from the cache and report differences near the end of the log. The cache can be cleared manually from the build page. Look under "More options" (upper-right).
 
 **CI Debug**: <a href="https://docs.travis-ci.com/user/running-build-in-debug-mode" target="_blank">Debugging Travis-CI failures</a> can be awkward. To simplify things, if a formal check fails, CI scripts attempt to upload the failure traces using https://transfer.sh/. Look for messages near the end of the log file containing links to the uploaded traces for download and debug.

ci/README.md

@@ -1,4 +1,3 @@
 This directory contains files that support continuous integration (CI) testing.
 Other files that support CI include
   - warp-v/.travis.yml
-  - warp-v/pre-commit

formal/.gitignore

@@ -4,13 +4,10 @@ complete
 /picorv32.v
 /disasm.s
 /disasm.o
-# These are pre-compiled by pre-commit so CI can run without SandPiper.
-#build\.sv
-#build_gen\.sv
-
-# Intermediate files for SandPiper pre-build
-/sp_obj/
 
 # Environment directories built by make_env
 /env
 /env_build
+
+# SandPiper(TM) SaaS Edition output directory
+/out

formal/Makefile

@@ -6,6 +6,12 @@ export PATH:=$(shell pwd)/env/bin:$(PATH)
 
 .PHONY: all compile verif env riscv-formal
 
+
+# Run SandPiper Cloud Edition(TM) (SandPiper(TM) in the cloud for open-source code).
+out/warp-v_formal.sv out/warp-v_formal_gen.sv: warp-v_formal.tlv ../warp-v.tlv
+	rm -rf out
+	curl -F 'warp-v_formal.tlv=@warp-v_formal.tlv' -F 'warp-v.tlv=@../warp-v.tlv' http://saas.makerchip.com/sandpiper | tar -zx && cat out/stdout
+
 env: env/PASSED
 
 # Use env/PASSED to indicate that the environment has been successfully built.
@@ -15,19 +21,14 @@ env/PASSED:
 
 riscv-formal: riscv-formal/README.md
 
-# Use riscv-formal to indicate that the git submodules have been installed.
+# Use riscv-formal/README.md to indicate that the git submodules have been installed.
 riscv-formal/README.md:
 	@# Just update timestamp if that's all that's needed, or install git submodules.
 	if [ -e riscv-formal/README.md ]; then touch riscv-formal/README.md; else git submodule init; git submodule update; fi
 
-compile: build.sv
-
-build.sv: warp-v_formal.tlv
-	rm -rf sp_obj
-	@# Invoke SandPiper. Need to provide input path reaching up the hierarchy to permit higher-level file inclusion.
-	sandpiper -i ../formal/warp-v_formal.tlv -o build.sv --obj sp_obj -p verilog
+compile: out/warp-v_formal.sv
 
-verif: checks.cfg genchecks.py build.sv env riscv-formal
+verif: checks.cfg genchecks.py out/warp-v_formal.sv out/warp-v_formal_gen.sv env riscv-formal
 	@# Should use this, but until Clifford accepts pull request, we have a local copy of genchecks.py.
 	@#python3 riscv-formal/checks/genchecks.py --basedir ../riscv-formal
 	python3 ./genchecks.py --basedir ./riscv-formal
@@ -36,5 +37,4 @@ verif: checks.cfg genchecks.py build.sv env riscv-formal
 all: verif
 
 clean:
-	rm build.sv build_gen.sv
-	rm -rf sp_obj
+	rm -rf out

formal/build.sv

@@ -1,3 +1,9 @@
+THIS FILE AND THE CORRESPONDING build_gen.sv ARE OBSOLETE.
+But before deleting, automate the build of the impl code.
+
+
+
+
 `line 2 "formal/warp-v_formal.tlv" 0 //_\TLV_version 1d: tl-x.org, generated by SandPiper(TM) 1.9-2018/02/11-beta
 
    // Configure for formal verification.

formal/checks.cfg

@@ -30,6 +30,6 @@ causal    10    28
 read_verilog @basedir@/../verilog/clk_gate.v
 read_verilog -sv @basedir@/../verilog/pseudo_rand.sv
 read_verilog -sv -I @basedir@/../verilog @basedir@/../wrapper.sv
-read_verilog -sv -I @basedir@/../verilog @basedir@/../build.sv
+read_verilog -sv -I @basedir@/../verilog @basedir@/../out/warp-v_formal.sv
 
 

formal/warp-v_formal.tlv

@@ -1,11 +1,11 @@
-\m4_TLV_version 1d: tl-x.org
+\m4_TLV_version 1d -p verilog: tl-x.org
 m4+definitions
    // Configure for formal verification.
    m4_define(['M4_TB'], 0)
    m4_define(['M4_FORMAL'], 1)
 \SV
    // Include WARP-V.
-   m4_include_lib(['../warp-v.tlv'])
+   m4_include_lib(['./warp-v.tlv'])
 m4+module_def
 \TLV
    m4+cpu()