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

Hi Yaniv,

 

What will be if rst_b or start_ev are non-deterministic free variables?
You will have to write different checkers for different situations.

 

Thanks,

Dmitry

 

________________________________

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of Fais Yaniv
Sent: Wednesday, November 14, 2007 6:14 PM
To: sv-ac@server.eda.org
Subject: [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 <http://www.mailscanner.info/> , and is

believed to be clean. 
---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

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