Assume when signal falls it will remain low until two periods of clock have passed

Assume when signal falls it will remain low until two periods of clock have passed

Hello I am fairly new to SVA. I was having trouble defining an assume property.

Basically I have a pulse sync module, and the design can only handle one incoming signal at a time, meaning that the incoming async_signal has to be at least two clock periods apart.

For my assumption, I want to say that when the input async_signal falls, it will stay low until it detects 3 rising edges of clock. Keep in mind that the mclk I am using is running at a higher frequency than what the clock is running at.

This is the current property that I am using to apply this, but I doesn’t seem to be working.
assume property (@(edge mclk) $fell(async_signal) |-> (!async_signal throughout ($rose(clock)[*3])));

This is the cover I am using to test it:
cover property (!async_signal ##[0:] async_signal ##[0:] !async_signal ##[0:$] async_signal);

If anyone has suggestions on how I can fix this or have any tips on best practices I would greatly appreciate it.

In reply to Andrew R:


// You have 2 clock systems 
// Use as sampling clock the slower clock in your consequent, 
// but use the negedge of clock to sample the clock signal.
assume property (@(edge mclk) $fell(async_signal) |-> 
  @(posedge clk) (!async_signal throughout ($rose(clock, @(negedge clock))[*3])));

// On the cover, I would use the got operator 
cover property (@(posedge mclk) async_signal[->2]);
// goto: a[->1] is same as !a ##[0:$] a 
//       a[->2] is same as !a ##[0:$] a ##1 !a ##[0:$]a 
 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Thank you for the fast reply.

Using a different clock in the consequent gives me the following error:
The clock flow cannot change in the RHS of |-> operator

In reply to Andrew R:
Changed from |-> @(posedge clk)
TO
|-> @(posedge clock)
1800 allows the clock flow cannot change in the RHS of |-> operator.
This was a restriction in the previous version of 1800.
Some tools may not have updated that feature. If they did not,
use the " |=> " instead of "|-> "


module m; 
  bit mclk, async_signal, clock;
  assume property (@(edge mclk) $fell(async_signal) |-> 
                   @(posedge clock) (!async_signal throughout ($rose(clock, @(negedge clock))[*3]))); 
endmodule  

Works OK.
BTW, we do not address specific tools in this forum, but we can say things like “my simulator” does this or that, but keep the identity hidden.

Ben SystemVerilog.us