diff options
| author | Clifford Wolf <clifford@clifford.at> | 2014-03-13 13:12:06 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2014-03-13 13:12:06 +0100 |
| commit | 7a1ac1120351d5cf0de2c9173fb7353795b0137e (patch) | |
| tree | b8f2280723bec260be72002745c3d94b5afe03c9 /frontends/verific/test_navre.ys | |
| parent | 542afc562fa8b828f3c87e9dbe47a373ac09f147 (diff) | |
Added test_navre.ys for verific frontend
Diffstat (limited to 'frontends/verific/test_navre.ys')
| -rw-r--r-- | frontends/verific/test_navre.ys | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/frontends/verific/test_navre.ys b/frontends/verific/test_navre.ys new file mode 100644 index 00000000..9e11cde0 --- /dev/null +++ b/frontends/verific/test_navre.ys @@ -0,0 +1,17 @@ +verific -vlog2k ../../../yosys-bigsim/softusb_navre/rtl/softusb_navre.v +verific -import 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 |