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.
// 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
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.