diff options
Diffstat (limited to 'frontends/verific/test_navre.ys')
| -rw-r--r-- | frontends/verific/test_navre.ys | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/frontends/verific/test_navre.ys b/frontends/verific/test_navre.ys deleted file mode 100644 index a56b725a..00000000 --- a/frontends/verific/test_navre.ys +++ /dev/null @@ -1,18 +0,0 @@ -verific -vlog2k ../yosys-bigsim/softusb_navre/rtl/softusb_navre.v -verific -import softusb_navre - -memory softusb_navre -flatten softusb_navre -rename softusb_navre gate - -read_verilog ../yosys-bigsim/softusb_navre/rtl/softusb_navre.v -cd softusb_navre; proc; opt; memory; opt; cd .. -rename softusb_navre gold - -expose -dff -shared gold gate -miter -equiv -ignore_gold_x -make_assert -make_outputs -make_outcmp gold gate miter - -cd miter -flatten; opt -undriven -sat -verify -maxsteps 5 -set-init-undef -set-def-inputs -prove-asserts -tempinduct-def \ - -seq 1 -set-at 1 in_rst 1 # -show-inputs -show-outputs |