Subject: Re: Assertion requirements
From: Adam Krolnik (krolnik@lsil.com)
Date: Wed Jul 31 2002 - 07:26:24 PDT
Good morning Cindy;
In response to:
:>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.
You wrote:
>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?
This is an issue with ease of use - if you use assert_strobe semantics
when you write your assertions, then you have less chances of creating
an assertion with a race condition. For example.
You write an immediate assertion (in a clocked block) and it works
today, but tomorrow it fails. You discover that it needs the
combinatorial signal 'in_ready' to add another condition to either
the antecedent or consequent. If you add this combinatorial signal,
you now need to use assert strobe semantics because you need to
ensure that the combinatorial signal has the correct value.
Thus I am going to recommend a methodology of using assert_strobe
in preference to assert (immediate.)
>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"
> - "meta-assertions" that talk about things going on in the
> simulation, for
Which of the two will be most prevalent? Thus which should be the
easiest to type? I have written assertions for detecting glitches
and other non cycle based elements, but there are other ways to
do this without requiring assertions to be able to support this
as well.
:>> req -> {ack[*1:10]}
:>>Without any clarification/restriction, both properties will see
:>>'done' asserted at cycle 4 and indicate satisfaction/pass.
>correct. this is the semantics of sugar.
This does not match design intent - pipelined protocol utilize a fifo
(1 or more registers) to maintain inorder state and data returns
(the handshake.)
You example of:
'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));
Does not provide a compelling case for complex assertions (sequences,
etc.)
>if we add an operator
>which has fifo semantics, it will need to have such a parameter.
> [ defining the limit of the fifo.]
I agree that this is probably the way to go - With this many more things
can be done with assertions without resorting to having to build
code like the example (which somewhat defeats the purposes of assertions
- simple and easy to express properties about a design.)
Thanks Cindy for showing how sugar addresses many of the needs I see for
this language. I hope that we can soon address how this all can fit into
SystemVerilog.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Wed Jul 31 2002 - 07:28:22 PDT