Limitations of concurrent SVAs within procedural block

SystemVerilog
,
1

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 ?

2

In reply to MICRO_91:

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.

or Links_to_papers_books - Google Docs

3

In reply to ben@SystemVerilog.us:

Thanks Ben.
Any suggestions on when should a user consider using procedural approach ?

4

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

5

In reply to ben@SystemVerilog.us:

Hi Ben,
While revisiting this thread I noticed that the concurrent assertion within always procedural block is equivalent to overlapping implication :


  property multi_clk1;  
    @(posedge clk1) a |-> @(posedge clk2) b;
  endproperty

So if clk1 and clk2 were of same time period


  always #5 clk1 = !clk1;
  always #5 clk2 = !clk2;

Via mc2 , both ‘a’ and ‘b’ are evaluated on overlapping posedge of clk1 and clk2 at time: 5 , 15 , 25 , 35 …

If I were to use non-overlapping implication


  property multi_clk2;  
    @(posedge clk1) a |=> @(posedge clk2) b;
  endproperty

Would it be possible to achieve non-overlapping equivalent using mc2 ( concurrent assertion within always procedural block ) ?