I have a situation, since the actual code is lot complex I am representing the problem as a high level model.
This is the pseudocode of what my problem is:
property p(a,b,c,d); //I want this property to be concurrent and on clk since I am using throughout operator
@(posedge clk) disable iff (!resetn)
a ##0 b |=> not(c throughout d[->1]);
endproperty
always @ (posedge clk) begin
.
.//here we decide which signals from the bus should be send as a,b,c and d for checking in the assertion
./
.
assert property(p(a,b,c,d)); //I want this current run of the assertion to stop and die as soon as d triggers (since this is in always block on a clk)
.
.
.
end
How can we implement a solution for the above problem.
Thanks for the help in advance.
Thanks for inputs. I have looked that up, with accept_on/reject_on we can manipulate the assertion result. That should do.
Lets say for a moment, the off/on (accept/reject) behavior is a dont care.
In that case we just simply assert a concurrent property (it has to be made concurrent because we want it to consume time since we used throughout)inside a clocked always block.
My goal is to rewrite that concurrent assertion with an equivalent task (as tasks can also consume time).Any suggestions on how to do this would be great.