yosys/examples/smtbmc/demo4.smtc

12 lines
151 B
Plaintext
Raw Permalink Normal View History

2016-08-27 07:30:36 -05:00
initial
assume [rst]
always -1
assume (not [rst])
assume (=> [-1:inv2] [inv2])
final -2
assume [-1:inv2]
assume (not [-2:inv2])
assert (= [r1] [r2])