Subject: Re: Assertion requirements
From: Adam Krolnik (krolnik@lsil.com)
Date: Mon Jul 29 2002 - 09:25:16 PDT
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 : Mon Jul 29 2002 - 09:27:10 PDT