Hi,
Although the LRM allows using concurrent assertions within procedural block ( always@(clocking_event) ) as well as outside them,
I was wondering if the procedural one has any limitations over the other.
I was trying out a few codes for multiclocked SVAs
always #5 clk1 = !clk1;
always #10 clk2 = !clk2;
property multi_clk;
@(posedge clk1) a |-> @(posedge clk2) b;
endproperty
property multi_clk2;
@(posedge clk2) b;
endproperty
mc1:assert property(multi_clk) $display("T:%0t mc1 succeeds",$time);
else $display("T:%0t mc1 fails",$time);
always@(posedge clk1) begin
if( a ) begin
mc2:assert property(multi_clk2) $display("T:%0t mc2 succeeds",$time);
else $display("T:%0t mc2 fails",$time);
end
end
initial begin
#1; a = 1; b = 1;
#10; $finish();
end
According to LRM is mc2 considered legal ? I observe discrepancy across tools.
If no, can I conclude that for multiclocked properties one should use concurrent assertions outside procedural block ?
Are there any more advantages of one over the other ?
The code is legal and the tools give identical results.
T:10 mc2 succeeds
T:10 mc1 succeeds
The issue you are experiencing in Edaplayground are the switches needed.
Make sure to add for vcs -lca -assert svaext
In the future, if you post code that you tried on EdaPlayground, please provide the link to the code and waveforms (if you generate any). I use the action block with a pass/fail variable.
int pass, fail;
assert property(p) pass=pass+1; else fail=fail+1;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
..
end
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
In reply to MICRO_91:
Procedural concurrent assertions have been incorporated as an option to empower users to assert a property once a specific point deep within an FSM is reached. For instance, consider a complex traffic light controller that is designed with multiple FSMs, one for each intersection. When Intersection A transitions to the AMBER state, and if information about the states of the other intersections is available, a user can then trigger an assertion regarding the expected states of Intersections B, C, and D in the upcoming states.
Ben