+ # the following is needed for induction, where an unreachable state
+ # (memory and holding register differ) is turned into an illegal one
+ # first, get the value stored in our memory location, using its debug
+ # port
+ stored = Signal.like(dut.q)
+ m.d.comb += dut.dbg_a.eq(a_const)
+ m.d.comb += stored.eq(dut.dbg_q)
+ # now, ensure that the value stored in memory is always in sync
+ # with the holding register
+ with m.If(wrote):
+ for i in range(len(dut.we)):
+ with m.If(we_mask[i]):
+ m.d.sync += Assert(d_reg == stored[i*gran:i*gran+gran])
+
+ self.assertFormal(m, mode="prove", depth=2)