+
+ if platform == "formal":
+ # pass upstream state to the memories, so they can ensure that
+ # their state are in sync with upstream, for induction
+ m.d.comb += [
+ # address and write lane under test
+ mem0.dbg_addr.eq(self.dbg_addr),
+ mem1.dbg_addr.eq(self.dbg_addr),
+ mem0.dbg_we_mask.eq(self.dbg_we_mask),
+ mem1.dbg_we_mask.eq(self.dbg_we_mask),
+ # upstream state
+ mem0.dbg_data.eq(self.dbg_data),
+ mem1.dbg_data.eq(self.dbg_data),
+ # the memory, on which the write ends up, depends on which
+ # phase it was written
+ mem0.dbg_wrote.eq(self.dbg_wrote & ~self.dbg_wrote_phase),
+ mem1.dbg_wrote.eq(self.dbg_wrote & self.dbg_wrote_phase),
+ ]
+ # sync phase to upstream
+ m.d.comb += Assert(self.dbg_phase == phase)