[sv-ac] checkers (1900) , SV-AC meeting 2007-11-13

Hi,

On yesterday's meeting I've said I'll send an example illustrating usage
of deterministic variable and non-deterministic variables (which I call
"free") in the same checker to illustrate my point, here is my modified
example taken from the original proposal page 13.

checker data_legal_within_range(bit clk,start_ev, end_ev, untyped
in_data, out_data,addr);
 
    // deterministic variable used for modeling some counter which
counts cycles since last start_ev
    bit [3:0] cnt = 4'd0;
    always @(posedge clk or negedge rst_b)
       if (rst_b)
         cnt <= 4'd0;
       else
         cnt <= ($rose(start_ev) ? 4'd0 : cnt+1'b1);
 
   // non-deterministic free variables
   // this first is used instead of a local variable as in the original
example and the second is used as another limitation under assumption
    const freevar bit [$bits(in_data)-1:0] mem_data;
    const freevar bit [$bits(addr)-1:0] free_addr;
 
    sequence transaction();
        start_ev && (in_data == mem_data) && (addr==free_addr) ##1
end_ev[->1];
    endsequence
    // same as the original example but we also add an assertion that
the range may not be more than 10 cycles
    // this can also be written using another local variable...
    a1: assert property (@(posedge clk) transaction() |-> (out_data ==
mem_data) and (cnt < 10) );
     
    // two start_ev can't be more than 15 cycles apart (not including
reset) - also avoid overflow for this simple example
    a2 : assert property (@(posedge clk) cnt < 15);
 
    // have this assertion only for addresses in this range
    a3 : assume property (@(posedge clk) free_addr < 0xff00);
 
endchecker : data_legal_within_range
 
The semantic of the above example is exactly as if instead of "bit cnt"
it was written "freevar bit cnt" and the always block would be changed
to always_check.
 
As you can see semantically there is no fundamental change here but
syntactically it is much more clear which variables are non
deterministic and which are deterministic, I found it very confusing to
see many "freevars" which are in fact deterministic,for example the last
two examples of the proposal (page 21 my_check and page 22 check_window)
have many freevars defined inside of them but actually all of those are
deterministic !
 
I agree however that allowing this makes the definition more complicated
since non freevars have normal simulation semantics and there is the
question what if a non deterministic variable is being assigned to a
deterministic variable but since verilog is used not only for simulation
I think it should be essentially the same as if a primary input is being
assigned to a deterministic variable in a formal verification
environment.
 
 
Yaniv
 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.