- # our debug port allow the formal engine to inspect the content of
- # a fixed, arbitrary address, on our memory blocks.
- # wire it to their debug ports.
- m.d.comb += mem1.dbg_a.eq(self.dbg_a)
- m.d.comb += mem2.dbg_a.eq(self.dbg_a)
- m.d.comb += self.dbg_q1.eq(mem1.dbg_q)
- m.d.comb += self.dbg_q2.eq(mem2.dbg_q)
+
+ if platform == "formal":
+ # the following is needed for induction, where an unreachable
+ # state (memory and holding register differ) is turned into an
+ # illegal one
+ # first, get the values stored in our memory location, using its
+ # debug port
+ m.d.comb += mem1.dbg_a.eq(self.dbg_addr)
+ m.d.comb += mem2.dbg_a.eq(self.dbg_addr)
+ stored1 = Signal(self.data_width)
+ stored2 = Signal(self.data_width)
+ m.d.comb += stored1.eq(mem1.dbg_q)
+ m.d.comb += stored2.eq(mem2.dbg_q)
+ # now, ensure that the value stored in the first memory is always
+ # in sync with the holding register
+ with m.If(self.dbg_wrote):
+ for i in range(self.we_width):
+ with m.If(self.dbg_we_mask[i]):
+ m.d.comb += Assert(
+ self.dbg_data == stored1.word_select(i, gran))
+ # same for the second memory, but one cycle later
+ with m.If(Past(self.dbg_wrote)):
+ for i in range(self.we_width):
+ with m.If(self.dbg_we_mask[i]):
+ m.d.comb += Assert(
+ Past(self.dbg_data) == stored2.word_select(i, gran))