Subject: Re: Assertion requirements
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Wed Jul 31 2002 - 06:58:18 PDT
adam,
>:>#4 Sugar Verification directives shall be simulated using
>:>assert_strobe
>:>semantics - they should simulate at the end of the timestep.
>
>This request is for an example like this:
>
>always @(a or b or c or d)
> begin
> if (a)
> begin
> g = 1'b0;
> assert( !b |-> {!c; !c}) //(1)
> @@(posedge clk) else
> $error("C must be low for two cycles when B is not true.");
> ...
>
>If C is driven from:
>
> assign c = reg_a | reg_b & inp_c;
>
>Then, the assertion may fail if the assertion evaluates 'c' before the
>assign statement. With strobe sematics, the next cycle of the sequence
>will evaluate last.
i see what you mean, but it seems to me that the user has the ability to
prevent this situation already by using assert_strobe. why change the
meaning of assert under certain conditions? i can't think of an example
off the top of my head, but i can envision a situation where the user wants
to use assertions to detect race conditions in the verilog code. if we
define that assert is equivalent to assert_strobe, you would lose this
ability.
in my view, there are two uses of assertions:
- those that make a statement about properties the design is supposed to
have. these assertions should use "synthesis semantics", that is, they
should view the design at the same level of granularity as the synthesis
tools. for this type of assertion, you would want to ignore the
sensitivity list altogether - which i think is equivalent to your strobe
semantics.
- "meta-assertions" that talk about things going on in the simulation, for
instance, race conditions. these assertions should use "simulation
semantics", that is, they should view the design at the same level of
granularity as the simulation tools. for this type of assertion, the whole
point is to see what is going on inside the time ticks of simulation. in
this case, you do not want to impose strobe semantics on the user.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
>>#6 Extend Sugar to support overlapping properties with fifo
>>semantics
>I am not asking for more semantics (past state) than are already
>inherent.
>I am asking to clarify what happens for this type of assertion.
>
>always req |-> {[*1:10]; done} (3)
>
>> clk __1 __2 __3 __4 __5 __6 __7 __
>> ____| |__| |__| |__| |__| |__| |__| |__|
>> _____ _____
>> req ____| |_____| |__________________________________
>> ___________
>> done ______________________| |______________________
>> _____
>> done2 ______________________| |____________________________
>
>This property will run/execute/evaluate/thread twice (cycles 1, 3).
it is true that the property is relevant only in cycles 1 and 3. however,
as i stated before, an efficient implementation will not need two threads.
one checker is enough to check this formula, in simulation as well as in
formal verification. this is true for a formula which excepts a one-to-one
correspondence between reqs and dones as well as one that does not. if
people are interested, i can send a separate note showing how this is done.
>>Without any clarification/restriction, both properties will see 'done'
>>asserted at cycle 4 and indicate satisfaction/pass.
correct. this is the semantics of sugar.
>>My solution to this problem was to only allow *one*
>>property/evaluation/thread
>>to see/consume/find an event in a variable time window. Thus only
>>the property started on cycle 1 would complete on cycle 4. The property
>>started on cycle 3 would complete on cycle 5 with the second 'done'.
i understand what you want. i am merely saying that the semantics of "->"
don't work this way, but that we can check the property in other ways.
>>:furthermore, you probably want the fifo semantics to say not only
>>:whether every req got an ack, but also whether or not there were
>>:too many acks, right?
>>
>>Yes, that's what the bidirectional implication operator is for, correct?
>>
>> always req <-> {[*1:10]; done} (4)
this is bad sugar. the <-> operator works only between two booleans, and
(p <-> q) is equivalent to ((p -> q) && (q -> p)). note that the sere
implication operator |-> works between two seres, and requires the second
to hold at the cycle where the first completes. so even if there were a
"bidirectional" sere implication operator, it would require you to start
looking for req the cycle of done, which is not what you want.
>>:furthermore, sugar deals with finite state. putting the onus on the
>>:implication operator as you request would seem to require that any
>>:number of outstanding reqs are allowed (for instance, for the property
>>:always (req -> eventually! ack), in which there is no bound on the
>>:number of cycles between a req and its ack).
>>
>>If one has no limit on outstanding requests, then there is no limit on
>>the RTL (design storage.) Since there is a limit on the design storage,
>>there is always limit on the number of outstanding requests. This should
>>also be a property specific to the design.
of course. all i meant was that there is no place in the -> operator to
specify that limit (this is not the main problem with giving these
semantics to ->, just a minor additional point). if we add an operator
which has fifo semantics, it will need to have such a parameter.
>>:Possible today by combining modeling with the temporal assertion.
>>
>>2 questions:
>>
>>1. Could you show the modeling to support property #4?
>>2. How would this modeling be done in SystemVerilog?
'define MAX 8
'define ERRORVAL -1
'define incr(n) (n+1>MAX)?ERRORVAL:n+1
'define decr(n) (n-1<0)?ERRORVAL:n-1
integer i;
initial i = 0;
always @(posedge clk)
if (req && done)
i = #0 i;
else if (req)
i = #0 incr(i);
else if (done)
i = #0 decr(i);
assert never (i==ERRORVAL);
assert always (endofsimulation -> (i=0));
disclaimer: sugar requires bounded integer ranges rather than unbounded
integers. other than that, the above code is pure sugar, and as you can
see, doing it in systemverilog would be pretty much the same.
-----------------------------------------------------------------------
>>#8. Support procedural systemVerilog assertions as if they were
>>declarative and contain an antecedent equivalent to the position
>>where they are located in the code.
>
>:i don't understand this, nor do i understand the justification, in
>:which you say that "the example may fail falsely". i assume that by
>:"fail falsely" you mean "not according to the intention of the user"?
>
>See the above discussion about 'disable'. This requirement is an
>attempt to fix simulation sematic problems. Formal tools do not have
>delayed signals or race conditions about them.
see my response to #4 above. perhaps simulation semantics are not always
problems to be fixed, but problems to be detected by the assertions?
-----------------------------------------------------------------------
>>#9. Extend sugar Verification directives to include optional
>>clocking specification (to override the presumed global clocking signal.)
>
>:sugar already supports clocking a property, with syntax similar to
>:that you
>
>I am looking for a way to specify a
>global/default clock for a module/system so that I don't have to
>have every assertion specify a clock.
sugar supports this as well, using the syntax:
default clock = clka;
regards,
cindy.
Cindy Eisner
Formal Methods Group Tel: +972-4-8296-266
IBM Haifa Research Laboratory Fax: +972-4-8296-114
Haifa 31905, Israel e-mail:
eisner@il.ibm.com
Adam Krolnik <krolnik@lsil.com>@dts0.lsil.com on 29/07/2002 19:25:16
Sent by: krolnik@dts0.lsil.com
To: Cindy Eisner/Haifa/IBM@IBMIL
cc: sv-ac@eda.org, Adam Krolnik <krolnik@lsil.com>
Subject: Re: Assertion requirements
Good morning Cindy;
[Cindy's comments are prefixed with ':', my previous comments are '>']
:>#4 Sugar Verification directives shall be simulated using
:>assert_strobe
:>semantics - they should simulate at the end of the timestep.
:i do not agree with this. if sugar code can be embedded in
:procedural
:code, then it should have semantics which are consistent with other
:embedded assertions. for instance, for the following code:
This request is for an example like this:
always @(a or b or c or d)
begin
if (a)
begin
g = 1'b0;
assert( !b |-> {!c; !c}) //(1)
@@(posedge clk) else
$error("C must be low for two cycles when B is not true.");
...
If C is driven from:
assign c = reg_a | reg_b & inp_c;
Then, the assertion may fail if the assertion evaluates 'c' before the
assign statement. With strobe sematics, the next cycle of the sequence
will evaluate last.
This assertion may also fail due to a race between the block evaluating
'a' and a block assigning it. The assertion statement could have been
improperly started since 'a' should be 0 for the current cycle. E.g.
(for effect) if 'a' was driven by:
assign #1 a = ~reg_a;
Then the always block above would evaluate twice (if b, c, d changed
at the clock.) Since 'a' is evaluated 1 tick later. We would start the
assertion after b or c or d changed, and then we would reevaluate a
and have to follow the code. This is Harry's recommendation to fix
problems like this:
always @(a or b or c or d)
begin
disable check_c;
if (a)
begin
g = 1'b0;
check_c: assert( !b |-> {!c; !c}) //(2)
@@(posedge clk) else
$error("C must be low for two cycles when B is not true.");
The disable statement will cancel any started assertions so that
we don't allow an assertion to run with glitch values.
**NOTE: The use of this technique prevents effective use of the
multi-cycle sequences if the assertion can be started the next
cycle. The 'disable' statement would kill all started assertions,
even those started in past cycles.
[This is also a reason to prefer declarative assertions since you won't
have this problem.]
-------------------------------------------------------------
>#6 Extend Sugar to support overlapping properties with fifo
>semantics
:giving fifo semantics to the -> operator would pull the rug out from
:under
:the whole semantic foundation of sugar. the semantics of a sugar
:property
:at a given cycle depend only on the current and future state, not on
:the
:past. (if you want to access past values of a signal, you must go
:through
I do not believe it is that drastic (but I can not write the math behind
this request...)
I am not asking for more semantics (past state) than are already
inherent.
I am asking to clarify what happens for this type of assertion.
always req |-> {[*1:10]; done} (3)
> clk __1 __2 __3 __4 __5 __6 __7 __
> ____| |__| |__| |__| |__| |__| |__| |__|
> _____ _____
> req ____| |_____| |__________________________________
> ___________
> done ______________________| |______________________
> _____
> done2 ______________________| |____________________________
This property will run/execute/evaluate/thread twice (cycles 1, 3).
Without any clarification/restriction, both properties will see 'done'
asserted at cycle 4 and indicate satisfaction/pass.
My solution to this problem was to only allow *one*
property/evaluation/thread
to see/consume/find an event in a variable time window. Thus only
the property started on cycle 1 would complete on cycle 4. The property
started on cycle 3 would complete on cycle 5 with the second 'done'.
:furthermore, you probably want the fifo semantics to say not only
:whether every req got an ack, but also whether or not there were
:too many acks, right?
Yes, that's what the bidirectional implication operator is for, correct?
always req <-> {[*1:10]; done} (4)
What does the above property do (pass,fail) when applied to the above
waveforms (using 'done'?) (using 'done2'?)
The waveform 'done' is correct. The waveform 'done2' is incorrect.
:furthermore, sugar deals with finite state. putting the onus on the
:implication operator as you request would seem to require that any
:number of outstanding reqs are allowed (for instance, for the property
:always (req -> eventually! ack), in which there is no bound on the
:number of cycles between a req and its ack).
If one has no limit on outstanding requests, then there is no limit on
the RTL (design storage.) Since there is a limit on the design storage,
there is always limit on the number of outstanding requests. This should
also be a property specific to the design.
I am glad to see that you understand the usefulness of fifo semantics.
I understand (having implemented them) that fifo semantics are extremely
useful and common (often used.)
:Possible today by combining modeling with the temporal assertion.
2 questions:
1. Could you show the modeling to support property #4?
2. How would this modeling be done in SystemVerilog?
-----------------------------------------------------------------------
>#8. Support procedural systemVerilog assertions as if they were
>declarative and contain an antecedent equivalent to the position
>where they are located in the code.
:i don't understand this, nor do i understand the justification, in
:which you say that "the example may fail falsely". i assume that by
:"fail falsely" you mean "not according to the intention of the user"?
See the above discussion about 'disable'. This requirement is an
attempt to fix simulation sematic problems. Formal tools do not have
delayed signals or race conditions about them.
-----------------------------------------------------------------------
>#9. Extend sugar Verification directives to include optional
>clocking specification (to override the presumed global clocking signal.)
:sugar already supports clocking a property, with syntax similar to
:that you
In the same way that formal tools ask one to specify a global/default
clock to begin verification, I am looking for a way to specify a
global/default clock for a module/system so that I don't have to
have every assertion specify a clock.
For example, I may have a system composed of modules with
different coding styles. Thus I may have a module receive inputs
delayed from the clock edge. E.g.
assign #1 the_output = a | b;
I may want to specify all module assertions use the clock equivalent
to the statement:
wire #2 assert_clock = clk;
Of course formal tools do not need the notion of delay, but simulation
tools may.
Thanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Wed Jul 31 2002 - 07:04:04 PDT