summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-03-13 13:12:06 +0100
committerClifford Wolf <clifford@clifford.at>2014-03-13 13:12:06 +0100
commit7a1ac1120351d5cf0de2c9173fb7353795b0137e (patch)
treeb8f2280723bec260be72002745c3d94b5afe03c9
parent542afc562fa8b828f3c87e9dbe47a373ac09f147 (diff)
Added test_navre.ys for verific frontend
-rw-r--r--frontends/verific/test_navre.ys17
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