# Equivalance check script that creates a miter circuit and proves used | |
# temporaly induction that the miter circuit never asserts. | |
hierarchy | |
proc | |
clk2fflogic | |
miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter | |
sat -prove trigger 0 -verify -tempinduct miter |