2014-03-13 07:12:06 -05:00
|
|
|
verific -vlog2k ../../../yosys-bigsim/softusb_navre/rtl/softusb_navre.v
|
|
|
|
|
verific -import softusb_navre
|
|
|
|
|
|
2014-03-16 11:05:05 -05:00
|
|
|
memory softusb_navre
|
2014-03-13 07:12:06 -05:00
|
|
|
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
|
