- # 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))
+ # pass our state to the device under test, so it can ensure that
+ # its state is in sync with ours, for induction
+ m.d.comb += [
+ # pass the address and write lane under test to both memories
+ mem1.dbg_addr.eq(self.dbg_addr),
+ mem2.dbg_addr.eq(self.dbg_addr),
+ mem1.dbg_we_mask.eq(self.dbg_we_mask),
+ mem2.dbg_we_mask.eq(self.dbg_we_mask),
+ # the second memory copies its state from the first memory,
+ # after a cycle, so it has a one cycle delay
+ mem1.dbg_data.eq(self.dbg_data),
+ mem2.dbg_data.eq(Past(self.dbg_data)),
+ mem1.dbg_wrote.eq(self.dbg_wrote),
+ mem2.dbg_wrote.eq(Past(self.dbg_wrote)),
+ ]