# Equivalance check script that creates a miter circuit and proves used
# temporaly induction that the miter circuit never asserts.
#
# This version of the tempinduct attempts to prove the induction starting at
# 32 steps, and only attempts a proof at an interval of 16 steps.  This enables
# a larger search space for models with large induction loops (e.g. larger
# counters).
hierarchy
proc
clk2fflogic
miter -equiv -flatten -ignore_gold_x -make_outputs -make_outcmp gold gate miter
sat -prove trigger 0 -verify -tempinduct -tempinduct-skip 1 -initsteps 32 -stepsize 16 miter