diff options
| author | Ahmed Irfan <ahmedirfan1983@gmail.com> | 2014-09-22 11:35:04 +0200 |
|---|---|---|
| committer | Ahmed Irfan <ahmedirfan1983@gmail.com> | 2014-09-22 11:35:04 +0200 |
| commit | d3c67ad9b61f602de1100cd264efd227dcacb417 (patch) | |
| tree | 88c462c53bdab128cd1edbded42483772f82612a /frontends/verific/test_navre.ys | |
| parent | b783dbe148e6d246ebd107c0913de2989ab5af48 (diff) | |
| parent | 13117bb346dd02d2345f716b4403239aebe3d0e2 (diff) | |
| download | yosys-d3c67ad9b61f602de1100cd264efd227dcacb417.tar.gz yosys-d3c67ad9b61f602de1100cd264efd227dcacb417.tar.bz2 yosys-d3c67ad9b61f602de1100cd264efd227dcacb417.zip | |
Merge branch 'master' of https://github.com/cliffordwolf/yosys into btor
added case for memwr cell that is used in muxes (same cell is used more than one time)
corrected bug for xnor and logic_not
added pmux cell translation
Conflicts:
backends/btor/btor.cc
Diffstat (limited to 'frontends/verific/test_navre.ys')
| -rw-r--r-- | frontends/verific/test_navre.ys | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/frontends/verific/test_navre.ys b/frontends/verific/test_navre.ys new file mode 100644 index 000000000..a56b725ac --- /dev/null +++ b/frontends/verific/test_navre.ys @@ -0,0 +1,18 @@ +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 |