tests/sat/expose_dff.ys

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