Follow-up model to common local variable assigned in one sequence and use that in another intersecting sequence

This is a follow-up model to the question
https://verificationacademy.com/forums/systemverilog/can-common-local-variable-be-assigned-one-sequence-and-use-another-intersecting-sequence
In the above link, I explain the SVA rules of local variables when using concurrent sequences with the and, or, intersect. In this post, I am showing 4 models

  • SVA Model
property p_and;
bit v;
$rose(a) |-> ((b, v=c) ##3 v==c)and (c ##1 (1, v=d) ##2 v==c);
endproperty
ap_and: assert property(@(posedge clk) p_and);
  • Equivalent SVA model in SVA
 property p_and_equivalent;
bit v1, v2;
$rose(a) |-> ((b, v1=c) ##3 v1==c)and (c ##1 (1, v2=d) ##2 v2==c);
endproperty
ap_and_equivalent: assert property(@(posedge clk) p_and_equivalent);
  • Desired task model to force the use of the same local variable in both sequences
  • Equivalent SVA model using tasks

The concept of the task models is explained in my paper Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy

The simulation model is below and at at http://SystemVerilog.us/vf/flow_and.sv
The simulation statistics are at http://SystemVerilog.us/vf/sim_stats.png

Key elements of these task models is the use of fork - join_none tasks and arguments passed by reference. I agree that it is hard to follow, and this is why SVA is nice in that it is rather compact.
However, understanding the model helps in writing better SVA code, my belief because you get a better understanding of the equivalent inner works. Note that the actual implementation by vendors is different; what I am showing is an equivalency. The model:


module top;
    `include "uvm_macros.svh"
    import uvm_pkg::*;
    bit clk, a, b;
    bit c, d;
    int err_count_task, err_count_sva;
    event e_tand, e_sva; 
    initial forever #10 clk = !clk;
    property p_and; 
        bit v; 
        $rose(a) |-> ((b, v=c) ##3 v==c)and (c ##1 (1, v=d) ##2 v==c);
    endproperty 
    ap_and: assert property(@(posedge clk) p_and);  

    property p_and_equivalent; 
        bit v1, v2; 
        $rose(a) |-> ((b, v1=c) ##3 v1==c)and (c ##1 (1, v2=d) ##2 v2==c);
    endproperty 
    ap_and_equivalent: assert property(@(posedge clk) p_and_equivalent);  


    //***********************DESIRED NON-SVA AND NON-EQUIVALENT MODEL
    // where local variables are visible in concurrent sequences 
    // (SVA handles this as separate copies for each sequence) 
    // $rose(a) |-> ((b, v=c) ##3 v==c)and (c ##1 (1, v=d) ##2 v==c);
    // Desired Equivalent model (with common local variable) 
    // ((b, v=c) ##3 v==c) 
    task automatic t_b(ref bit v, done, err); 
        if(b) begin  
          v=c;
          repeat(3) @(posedge clk) ;
          assert(v==c) else err=1;
          $display("%t t_b.v==%b err=%b", $realtime, v, err);
          done=1'b1;
        end
        else err=1'b1;
        done=1;
    endtask 

    // (c ##1 (1, v=d) ##2 v==c)
    task automatic t_c(ref bit v, done, err); 
        if(c) begin 
          @(posedge clk);
          v=d;  
          repeat(2) @(posedge clk) ;
          assert(v==c) else err=1'b1;
          $display("%t t_c.v==%b", $realtime, v);
          done=1'b1;
        end
        else err=1'b1;
        done=1'b1;
    endtask 

    task automatic t_and();
        bit z;
        bit done1, done2, err1, err2;  
        if($rose(a, @(posedge clk) )) begin : antc // antecedent match 
           fork 
              t_b(z, done1, err1);
              t_c(z, done2, err2);
           join_none
           wait(done1 && done2);
           p_nonSVA_Model: assert(err1==0 && err2==0) else begin 
             -> e_tand;
             err_count_task+=1'b1; 
           end 
        end : antc
    endtask 

    // ********************** TASK MODEL PER SVA RULES 
    // $rose(a) |-> ((b, v=c) ##3 v==c)and (c ##1 (1, v=d) ##2 v==c);
    task automatic t_sva(); 
      bit z1, z2;
      bit done1, done2, err1, err2; //z1, z2 local variables of the property        
      if($rose(a, @(posedge clk) )) begin // antecedent match 
        fork 
            t_b(z1, done1, err1); // Note the separate local variables passed to 
            t_c(z2, done2, err2); // each thread
        join_none
        wait(done1 && done2);
        p_model_sva: assert(err1==0 && err2==0) else begin 
          -> e_sva;
          err_count_sva +=1'b1; 
        end
      end
  endtask 

    always_ff @(posedge clk) begin
      fork
        t_and();   
        t_sva();
      join_none           
    end
    
    initial begin
      repeat (300) begin
        @(posedge clk);
        if (!randomize(a, b, c, d) with {
          a dist {1'b1 := 1, 1'b0 := 1};
          b dist {1'b1 := 1, 1'b0 := 0};
          d dist {1'b1 := 1, 1'b0 := 4};
        })
          `uvm_error("MYERR", "This is a randomize error");
      end
      $finish;
    end
  endmodule  

========================================================
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: