2 read_verilog expose_dff.v
5 expose -shared -evert-dff test1 test2
6 miter -equiv test1 test2 miter12
7 flatten miter12; opt miter12
9 expose -shared -evert-dff test3 test4
10 miter -equiv test3 test4 miter34
11 flatten miter34; opt miter34
13 sat -verify -prove trigger 0 miter12
14 sat -verify -prove trigger 0 miter34