In reply to ivomilev:
*In reply to ben@SystemVerilog.us:*I was wondering shouldn’t we have disable fork; just after join any in your example for asynchronous check. With disable fork, we will avoid assertion failure after the @(posedge c) occurrence.
If @(b) occurs in the same time step as @(c) then you would have an assertion failure.
The question then is: Should that be a failure? But in any case, after the join_any
we test for the fail task variable. This is s join_any. If you put the disable fork; just after join any then you would not test the assertion. Maybe you are suggesting the following instead.
assert1: assert property (@(posedge clk) $fell(a) |-> (b throughout c[->1]));
// Also, "stable" is defined as
// $stable returns true if the sampled value of the expression did not change between the
// sampled value at the previous cycle and the sampled value at the current cycle.
// Otherwise, it returns false. Thus,
assert_stable: assert property (@(posedge clk) ##1 $fell(a) |->
($stable(b) throughout c[->1]));
However, what you want is something that is asynchronous. For that, I suggest the use of tasks with fork/join_any. For example:
task automatic t1();
// bit fail;
fork
begin : check_stable
@(b) assert(!fail) else $display("b is unstable %t", $realtime);
// fail=1;
return; // maybe disable fork?
end : check_stable
begin : at_end
@(posedge c);
end : at_end
join_any
// assert(!fail) else $display("b is unstable %t", $realtime);
endtask
initial
forever @(negedge a) t1();