| 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 | |