Subject: Re: glitches and scope of assertions [Was: [sv-ac] Re: Action items for Rajeev Ranjan]
From: Adam Krolnik (krolnik@lsil.com)
Date: Fri Aug 23 2002 - 15:40:50 PDT
Good afternoon Ambar;
You write:
>The specific situation I was thinking of is where we may want to specify
>properties saying that there are no glitches on the module outputs. Yes
>the designer was supposed to register all outputs, but failed to do so.
I do not believe that an assertion construct is the proper construct
to be used to construct a glitch detection mechanism.
There are many methods available in the existing language to detect
pulse width violations, changes after a specific time window, etc.
I am worried that proposing a requirement for this would make an
assertion construct require yet more language to be written by
the designer. In my opinion the more one has to write, the weaker
the assertion construct.
>detecting glitches are not in
>the scope of the formal assertion-checking tools based on cycle-based
>semantics. Does it mean that the simulation based assertion verification
>also has to be restricted to cycle-based semantics?
It appears that cycle based assertion semantics have a large body of
experience that we can base our work on.
>2. I am wondering if there are a class of properties that we cannot
>express due to cycle-based semantics. For the average
>verification/designer guy trying to adopt such a standard, it may not be
>always obvious what such properties are. Failing to clarify the scope of
>assertions upfront may become a significant hindrance to its adoption.
I would hope that the people on the committee have experience with
assertion methods to be able to say:
Here is a class of properties that are common(useful) to write.
Without a construct like this-that, you will not be able to
(easily) write this class of properties/assertions.
I hope that we don't build proposals on speculation of what one
could/should do with the construct. Verilog is general enough to allow
assertions to be written. However as many can attest to, the result
is too large (and thus buggy). As assertion (code) size increases, so
does
the reluctance by designers to use them.
>3. I am also not sure what the proposal is on the table for expressing
>properties for purely combinational blocks. Do we have to specify an
>associated clock even for properties dealing with purely combinational
>blocks? Isn't that odd?
This is what I was proposing a requirement to have a global clocking
mechanism available for assertions. You want to have this so that you
can specify when assertions should be evaluated. For example, my system
uses assert_clock as a global clock (defined below.) Maybe we want this
method to be able to override any locally specified clock in addition
to supplying a clock for assertions without one.
wire #2 assert_clk = clk; // clk is the system/core/unit) clock.
I prevent all race conditions with registers combinatorial logic and
a little delay on system level inputs. You need to have a clocking
mechanism for even combinatorial only code as this example shows.
BTW, here is an interesting combinatorial case - this is real code.
Would you be able to put an assertion here?
// Input is expected to be decoded - ensure this is true.
function [1:0] encode4;
input [3:0] onehot; //assert always ($onehot(onehot));
case (1'b1) //synopsys full_case parallel_case
onehot[0] : encode4 = 2'd0;
onehot[1] : encode4 = 2'd1;
onehot[2] : encode4 = 2'd2;
onehot[3] : encode4 = 2'd3;
endcase
endfunction
Back to the example....
[This is contrived, but each case shows a possible real world problem.]
/*
If you get the message
CYCLE ERROR: test, 10, selects not onehot {s1,s2} = 0
There is a real problem, the inputs to the mux module are not exclusive
at a clock boundary.
If you get the message
ERROR: test.m1, 1, selects not onehot {s1,s2} = x
There may not be a real problem but a simulation artifact because the
inputs to the mux module are not yet stable.
*/
module test;
reg a, b, c;
reg s1, s2;
wire o;
mux m1 (o, a, b, s1,s2);
// Show potential for signals resetting with differently.
initial s1 = 1'b1;
initial s2 = #1 1'b0;
initial begin
#10; check_select(s1, s2); // Advance clock, check assertion.
a = 1'b1;
b = 1'b0;
s1 = 1'b1;
#10; check_select(s1, s2); // Advance clock, check assertion.
// Show potential for signals to arrive differently
// due to different number assign statements in the paths.
s2 = 1'b1;
#0 s1 = 1'b0;
#10; check_select(s1, s2); // Advance clock, check assertion.
// Show potential for system input to have io buffer delay.
s1 = 1'b1;
#1 s2 = 1'b0;
#10; check_select(s1, s2); // Advance clock, check assertion.
end
initial $monitor($stime,, "o = %0b, s1=%0b, s2=%0b\n", o, s1, s2);
task check_select;
input s1, s2;
begin
if (s1 ^ s2)
begin end
else // fall through if X's
$display("CYCLE ERROR: %m, time %0d, selects not onehot {s1,s2} =
%0b",
$stime, s1, s2);
end
endtask
endmodule
module mux(o, a, b, s1, s2);
output o;
input a, b;
input s1, s2; // these are onehot selects.
always @(s1 or s2)
begin
if (s1 ^ s2)
begin end
else // fall through if X's
$display("ERROR: %m, time %0d, selects not onehot {s1,s2} = %0b",
$stime, s1, s2);
end
assign o = s1 ? a : s2 ? b : 1'b0;
endmodule
I get this output:
Compiler version 6.0; Runtime version 6.0; Aug 23 17:32 2002
ERROR: test.m1, time 0, selects not onehot {s1,s2} = 1x
0 o = x, s1=1, s2=x
1 o = x, s1=1, s2=0
10 o = 1, s1=1, s2=0
ERROR: test.m1, time 20, selects not onehot {s1,s2} = 11
20 o = 0, s1=0, s2=1
ERROR: test.m1, time 30, selects not onehot {s1,s2} = 11
30 o = 1, s1=1, s2=1
31 o = 1, s1=1, s2=0
V C S S i m u l a t i o n R e p o r t
Thanks Ambar for bringing this issue up for discussion.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Aug 23 2002 - 15:45:09 PDT