@@ -154,9 +154,15 @@ def elaborate(self, platform):
154
154
m .d .comb += Assert (dut .r_rdy
155
155
.implies (dut .r_data == gold .r_data ))
156
156
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 ))
160
166
161
167
return m
162
168
@@ -215,8 +221,9 @@ def elaborate(self, platform):
215
221
m .d .comb += fifo .r_en .eq (1 )
216
222
if fifo .fwft :
217
223
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 )
220
227
with m .If (r_rdy ):
221
228
m .d .sync += [
222
229
read_1 .eq (read_2 ),
@@ -230,15 +237,28 @@ def elaborate(self, platform):
230
237
with m .If (Initial ()):
231
238
m .d .comb += Assume (write_fsm .ongoing ("WRITE-1" ))
232
239
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 ):
234
246
m .d .comb += Assert (read_fsm .ongoing ("DONE" ))
235
247
236
248
with m .If (ResetSignal (domain = self .w_domain )):
237
249
m .d .comb += Assert (~ fifo .r_rdy )
238
250
239
251
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 )
242
262
243
263
return m
244
264
0 commit comments