Hi, I have an asynchronous property that checks if the time interval from posedge signal_A to posedge signal_B is smaller than a time_val. Here, time_val is a dynamic value that can change during the run-time, by other means.
If time_val changes, I want the assertion abort from the currently running executions. I basically want the assertion to abort, not disabled. Meanly, it should continue to got triggered on next posedge signal_A, after any abort. How can I implement this behaviour in terms of property/assertion context, without using any task or always block.
accept_on ( expression_or_dist ) property_expr // if (expr==true), property is true vacuously
reject_on ( expression_or_dist ) property_expr // if (expr==true), property is false vacuously
sync_accept_on ( expression_or_dist ) property_expr //
reject_onsync_reject_on ( expression_or_dist ) property_expr
[quote] it should continue to got triggered on next posedge signal_A, after any abort. How can I implement this behaviour in terms of property/assertion context, without using any task or always block.
[/quote]
At every @(posedge signal_A) there is an attempt at then assertion regardless of previous attemts.
Thus, the “continue to got triggered” is meaningless unless you want to only start a new attempt after the conclusion of the current attempt. This is called exclusivity. I address that topic in my paper
SUPPORT LOGIC AND THE always PROPERTY
Provides examples of support logic needed for certain types of requirements where the strict use of only SVA does not cover.
realtime time_val; // Dynamically updated by other means
bit time_val_changed; // Generated with support logic
logic signal_A;
logic signal_B;
property P_max_time;
realtime time_A;
@(posedge signal_A) (1, time_A = $realtime()) |=> @(posedge event_B) ($realtime() - time_A <= time_val)
endproperty
A_max_time : assert property (sync_accept_on(time_val_changed) P_max_time);
// Check with vendor for support of this feature
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Dear @ben2 , thank you for your reply. However, your proposals work for expressions. Here, I want the assertion executions abort at the moment of an event. How can I abort from the assertion due an event? For example @(time_val) ? Can we somehow use events in your proposals (accept_on, etc.)?
Basically, I want to finish the assertion execution on two events. If @(time_val), then abort and succeed. If @(posedge signal_B), then succeed only if the max time check passes. Here, for checking, I need to check time_val in terms of events, because there might be other events similar to @time_val that can abort this assertion also.
We maybe use @(posedge signal_A or edge time_val), but how to know which of the two triggering events happened, then evaluate accordingly?
[YOU]... abort at the moment of an event.
[Ben] Create a support expression based on an event
[YOU] If @(time_val), then abort and succeed. If @(posedge signal_B),
then succeed only if the max time check passes.
[Ben] Note that "If @(time_val) creates a cancel var, then accept_on abort and succeed vacuously"
// Updated code
realtime time_val; // Dynamically updated by other means
bit time_val_changed; // Generated with support logic
bit cancel; // <-------------NEW variable ---------------------
event ;
logic signal_A;
logic signal_B;
always @(time_val) begin
cancel=1; #1 cancel=0;
end
property P_max_time;
realtime time_A;
@(posedge signal_A) (1, time_A = $realtime()) |=> @(posedge event_B) ($realtime() - time_A <= time_val)
endproperty
A_max_time : assert property (sync_accept_on(cancel) P_max_time);
// if cancel==1 assertion is true vacuously
// Check with vendor for support of this feature
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.