From 1800: Note that if code in the Reactive region modifies signals and causes another pass to the Active region to
occur, this still may create glitching behavior in observed deferred assertions, as the new passage in the
Active region may re-execute some of the deferred assertions with different reported results. In general,
observed deferred assertions prevent glitches due to order of procedural execution, but do not prevent
glitches caused by execution loops between regions that the assignments from the Reactive region may
cause.
In the Postponed region of each simulation time step, each pending final deferred assertion report that has
not been flushed from its queue shall mature. Then the associated subroutine call (or $error, if the assertion
fails and no action block is present) is scheduled in the same Postponed region, and the pending assertion
report is cleared from the appropriate process’s deferred assertion report queue. Due to their execution in the
non-iterative Postponed region, final deferred assertions are not vulnerable to the potential glitch behavior
previously described for observed deferred assertions
“async signal ‘b’ that should go high immediately as trigger ‘a’ goes high ideally”
Looks like ‘b’ is a buffered (delayed) version of ‘a’ which is the output of a flop.
The following @(posedge clk) a |-> ##[0:1] b;
does not “check for b to go high starting from 0 all the way to 1 clock cycle.
assuming your delay isnt greater than 1 clock cycle.”
It is not a continuous check. All it says is that in the Preponed Region, the sampled values of ‘a’ and ‘b’ have the same values in the current and next cycle.
‘b’ can glitch at any time between those sampled times.
I don’t think Maddy’s check is what I initially wanted.
I want to make sure b goes high before the next clock edge. Not at the clock edge.
Ideally I want to check if b goes high immediately as a goes high.
Yes, a is a flop out and b is a delayed combo out of a.
This is not an actual problem I observed. Something that I was thinking about.
Im thinking this won’t be an issue since there will be clk-to-q delay and a will be checked at next edge anyway. By that time b will be high.
So by this logic I think Maddy’s suggestion will work.
In reply to Adarsh24:
Actually, you do not need any assertion here.
Signal ‘a’ is an output of flop with a hold delay.
Signal ‘b’ is a delayed combo out of ‘a’.
Thus, what you have is basically a wire with internal delays.
The concern is a setup and hold, and this is best done by using the system functions.
module setup_time_check(input clk, data); // SystemVerilog.us/vf/hold.sv
timeunit 1ns; timeprecision 100ps;
let tSU=2ns;
let tHLD=2ns;
bit notifier1;
specify
$setuphold( posedge clk, data, tSU, tHLD, notifier1 );
endspecify
endmodule
module top2(output logic clk, d);
realtime duration= 2.0ns;
…
setup_time_check setup_time_check1(clk, d); // built in 1800 setup and hold
// *** If you insist on using assertions, then assert those properties
property hold_chk;
realtime clock_sample;
@(posedge clk) (1,clock_sample = $realtime) |->
@(d) ($realtime - clock_sample) >= duration;
endproperty : hold_chk
property setup_chk;
realtime clock_sample;
@(d) (1,clock_sample = $realtime) |->
@(posedge clk) ($realtime - clock_sample) >= duration);
endproperty : setup_chk
If you insist on using an assertion for your ‘a’ ‘b’ concern, then you can simply write
// +--+ +--+
// |FF|----a----(gate_delays)------b--->|FF|---c
// +--+ +--+
// at every clocking event the sampled value of 'a' == sampled value of 'b'
ap_ab: assert property(@ (posedge clk) a==b);