yosys/tests/sat/expose_dff.ys

16 lines
323 B
Plaintext
Raw Permalink Normal View History

2014-02-08 14:27:04 -06:00
read_verilog expose_dff.v
hierarchy; proc;;
expose -shared -evert-dff test1 test2
miter -equiv test1 test2 miter12
flatten miter12; opt miter12
expose -shared -evert-dff test3 test4
miter -equiv test3 test4 miter34
flatten miter34; opt miter34
sat -verify -prove trigger 0 miter12
sat -verify -prove trigger 0 miter34