16 lines
323 B
Plaintext
16 lines
323 B
Plaintext
|
|
||
|
|
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
|
||
|
|
|