tests/sat/counters.ys

   1
   2 read_verilog counters.v
   3 proc; opt
   4
   5 expose -shared counter1 counter2
   6 miter -equiv -make_assert -make_outputs counter1 counter2 miter
   7
   8 cd miter; flatten; opt
   9 sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs
  10