diff --git a/.travis.yml b/.travis.yml index 5014dbe..3391bb4 100644 --- a/.travis.yml +++ b/.travis.yml @@ -32,11 +32,11 @@ jobs : script: - sed -i "/-stage/c\ m4_define([\'M4_STANDARD_CONFIG\'], [\'1-stage\'])" /home/travis/build/$BUILD_PATH/formal/warp-v_formal.tlv - sed -i "/insn /c\insn 20" /home/travis/build/$BUILD_PATH/formal/checks.cfg - - PATH=/home/travis/build/$BUILD_PATH/formal/env/bin:$PATH bash -c 'make verif'; + - PATH=/home/travis/build/$BUILD_PATH/formal/env/bin:$PATH bash -c 'make tos_agree verif'; - script: - sed -i "/-stage/c\ m4_define([\'M4_STANDARD_CONFIG\'], [\'4-stage\'])" /home/travis/build/$BUILD_PATH/formal/warp-v_formal.tlv - sed -i "/insn /c\insn 29" /home/travis/build/$BUILD_PATH/formal/checks.cfg - - PATH=/home/travis/build/$BUILD_PATH/formal/env/bin:$PATH bash -c 'make verif'; + - PATH=/home/travis/build/$BUILD_PATH/formal/env/bin:$PATH bash -c 'make tos_agree verif'; name : "4 Stage - riscv-formal" # the structure for the YAML format is non-standard in some way, but Travis interprets it correctly # with both the scripts being run parallel under same stage (in Travis terminology) diff --git a/formal/Makefile b/formal/Makefile index 1630d48..d0aefd5 100644 --- a/formal/Makefile +++ b/formal/Makefile @@ -7,11 +7,15 @@ export PATH:=$(shell pwd)/env/bin:$(PATH) .PHONY: all clean compile verif env riscv-formal +# Agree to SandPiper ToS. +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 rm -rf out mkdir out - yes | sandpiper-saas -i warp-v_formal.tlv -f ../warp-v.tlv -o warp-v_formal.sv --outdir out --sv_url_inc --iArgs + sandpiper-saas -i warp-v_formal.tlv -f ../warp-v.tlv -o warp-v_formal.sv --outdir out --sv_url_inc --iArgs env: env/PASSED diff --git a/impl/Makefile b/impl/Makefile index edd7845..9f8c6dc 100644 --- a/impl/Makefile +++ b/impl/Makefile @@ -11,7 +11,7 @@ all: $(WARPV_OUT) # Run SandPiper Cloud Edition(TM) (SandPiper(TM) in the cloud for open-source code). out/%/status: warp-v_%.tlv ../warp-v.tlv - yes | sandpiper-saas -i $< -f ../warp-v.tlv -o warp-v_$(patsubst warp-v_%.tlv,%,$<).sv --outdir out --sv_url_inc --iArgs + sandpiper-saas -i $< -f ../warp-v.tlv -o warp-v_$(patsubst warp-v_%.tlv,%,$<).sv --outdir out --sv_url_inc --iArgs impl: vivado -mode tcl -source Vivado/impl.tcl diff --git a/tsmc16-12/Makefile b/tsmc16-12/Makefile index 5c3c11e..3d6cd52 100644 --- a/tsmc16-12/Makefile +++ b/tsmc16-12/Makefile @@ -11,7 +11,7 @@ all: $(WARPV_OUT) # Run SandPiper Cloud Edition(TM) (SandPiper(TM) in the cloud for open-source code). out/%/status: warp-v_%.tlv ../warp-v.tlv - yes | sandpiper -i $< -f ../warp-v.tlv -o warp-v_$(patsubst warp-v_%.tlv,%,$<).sv --outdir out --sv_url_inc --iArgs + sandpiper -i $< -f ../warp-v.tlv -o warp-v_$(patsubst warp-v_%.tlv,%,$<).sv --outdir out --sv_url_inc --iArgs impl: #vivado -mode tcl -source Vivado/impl.tcl