@@ -154,9 +154,15 @@ def elaborate(self, platform):
154154 m .d .comb += Assert (dut .r_rdy
155155 .implies (dut .r_data == gold .r_data ))
156156 else :
157- m .d .comb += Assert ((Past (dut .r_rdy , domain = self .r_domain ) &
158- Past (dut .r_en , domain = self .r_domain ))
159- .implies (dut .r_data == gold .r_data ))
157+ # past_dut_r_rdy = Past(dut.r_rdy, domain=self.r_domain)
158+ past_dut_r_rdy = Signal .like (dut .r_rdy , attrs = {"amaranth.sample_reg" : True })
159+ m .d [self .r_domain ] += past_dut_r_rdy .eq (dut .r_rdy )
160+
161+ # past_dut_r_en = Past(dut.r_en, domain=self.r_domain)
162+ past_dut_r_en = Signal .like (dut .r_en , attrs = {"amaranth.sample_reg" : True })
163+ m .d [self .r_domain ] += past_dut_r_en .eq (dut .r_en )
164+
165+ m .d .comb += Assert ((past_dut_r_rdy & past_dut_r_en ).implies (dut .r_data == gold .r_data ))
160166
161167 return m
162168
@@ -215,8 +221,9 @@ def elaborate(self, platform):
215221 m .d .comb += fifo .r_en .eq (1 )
216222 if fifo .fwft :
217223 r_rdy = fifo .r_rdy
218- else :
219- r_rdy = Past (fifo .r_rdy , domain = self .r_domain )
224+ else : # r_rdy = Past(fifo.r_rdy, domain=self.r_domain)
225+ r_rdy = Signal .like (fifo .r_rdy , attrs = {"amaranth.sample_reg" : True })
226+ m .d [self .r_domain ] += r_rdy .eq (fifo .r_rdy )
220227 with m .If (r_rdy ):
221228 m .d .sync += [
222229 read_1 .eq (read_2 ),
@@ -230,15 +237,28 @@ def elaborate(self, platform):
230237 with m .If (Initial ()):
231238 m .d .comb += Assume (write_fsm .ongoing ("WRITE-1" ))
232239 m .d .comb += Assume (read_fsm .ongoing ("READ" ))
233- with m .If (Past (Initial (), self .bound - 1 )):
240+
241+ cycle = Signal (range (self .bound + 1 ))
242+ m .d .sync += cycle .eq (cycle + 1 )
243+ with m .If (Initial ()):
244+ m .d .comb += Assume (cycle == 0 )
245+ with m .If (cycle == self .bound ):
234246 m .d .comb += Assert (read_fsm .ongoing ("DONE" ))
235247
236248 with m .If (ResetSignal (domain = self .w_domain )):
237249 m .d .comb += Assert (~ fifo .r_rdy )
238250
239251 if self .w_domain != "sync" or self .r_domain != "sync" :
240- m .d .comb += Assume (Rose (ClockSignal (self .w_domain )) |
241- Rose (ClockSignal (self .r_domain )))
252+ # rose_w_domain_clk = Rose(ClockSignal(self.w_domain))
253+ past_w_domain_clk = Signal ()
254+ m .d .sync += past_w_domain_clk .eq (ClockSignal (self .w_domain ))
255+ rose_w_domain_clk = (past_w_domain_clk == 0 ) & (ClockSignal (self .w_domain ) == 1 )
256+ # rose_r_domain_clk = Rose(ClockSignal(self.r_domain))
257+ past_r_domain_clk = Signal ()
258+ m .d .sync += past_r_domain_clk .eq (ClockSignal (self .r_domain ))
259+ rose_r_domain_clk = (past_r_domain_clk == 0 ) & (ClockSignal (self .r_domain ) == 1 )
260+
261+ m .d .comb += Assume (rose_w_domain_clk | rose_r_domain_clk )
242262
243263 return m
244264
0 commit comments