[sv-ac] Nondeterministic free variables

Hi Ed,

 

I would like to address our discussion at the last meeting concerning
non-deterministic free variables. You suggested to follow VIS convention
and to use a special function $nondet for non-deterministic free
variables.

 

My general comment is that $nondet is just a different notation, and I
don't see how this notation may solve the problem of simulating
non-deterministic free variables. One could use a default value for the
variable type instead of $nondet in simulation, etc, but the same thing
may be implemented using the syntax suggested in the proposal; both
implementations will likely result in false negatives.

 

Now I would like to address the problems I see when using VIS $nondet
function.

 

Citing VIS documentation:

"... a nondeterministic construct, $ND, has been added to Verilog to
specify nondeterminism on wire variables and is the only legal way to
introduce nondeterminism in VIS. For example, to require that the output
at a particular state is nondeterministically GO or NOGO, one can
introduce a new variable, r, and write the following Verilog fragment. 

assign r=$ND{GO,NOGO};
.
.
always@(posedge clk) begin
.
.
state = r;
.
.
end

"

In VIS a non-deterministic value may be assigned using continuous
assignment only, and therefore the non-determinism in sequential
variables will have to be coded explicitly:

 

freevar bit r1, x1 = r1;

freevar bit r2, x2 = r2;

assign r1 = $nondet(r1);

assign r2 = $nondet(r2);

always_check @clk begin

x1 <= x1 && something_else;

x2 <= x2 && something_else;

end

 

// Values of x1 and x2 are different in this example

 

instead of

 

freevar x1, x2;

always_check @clk begin

x1 <= x1 && something_else;

x2 <= x2 && something_else;

end

 

// Values of x1 and x2 are different in this example

 

as now.

 

Note that creating one non-determinitsic variable for all cases instead
of creating individual copy for each case will be a common bug, and this
bug will be very hard to catch. Compare:

 

freevar bit r, x1 = r, x2 = r; // One non-deterministic variable is used

assign r = $nondet(r);

always_check @clk begin

x1 <= x1 && something_else;

x2 <= x2 && something_else;

end

 

// Values of x1 and x2 are identical in this example

 

Thanks,

Dmitry

---------------------------------------------------------------------
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.