Subject: Re: Assertions requirements from Real Intent
From: Adam Krolnik (krolnik@lsil.com)
Date: Tue Jul 30 2002 - 10:11:27 PDT
Hi Rajeev;
>These assertions could also be used to EXPLICITY capture an input assumption
>used for logic/fsm simplification by a designer -- as made famous by the
>quote from Bob Bentley, Intel.
Could you provide the quote - I'm curious about this...
>an input assumption within a procedural block affects the entire design
Yes, this is the duality of an assumption (provided it is accurate)
that it specifies what one block expects. It thus should also become
an assertion for the driving block to satisfy.
input assumption === output assertion
output requirement === input assumption
For tools that can extract and propagate assumptions back to the
driving block and propagate output requirements into an assumption
to the receiving block the property set can be increased without
requiring an engineer to textually copy these. This is a good thing!
Engineers can complement the work of others...
You explained, "what does it mean to spread accept/reject
directives around the rtl" as:
>always @(posedge clk)
> case (state)
> IDLE:
> if (c1)
> MY_ASSERT: assert than within 20 cycles event e1 occurs
>
> READY:
> if (c2)
> accept(MY_ASSERT);
>
> BUSY:
> if (c3)
> reject(MY_ASSERT);
>
> ACK:
> if (c4)
> accept(MY_ASSERT);
A few questions:
What does signaling the acceptance, passing of an assertion buy you?
Would not resetting the assertion give you the same abilities (since
you
are not expecting to produce a side effect?)
What is the benefit to writing a property so intertwined with the design
itself?
It would be difficult to explain to someone what such a property is
doing given its mingling with the code.
I would label this as taking procedural assertions too far. This does
not show a designer has considered what the real property may be but
may have instead found this to not fail (yet) in his simulations.
Good properties are written with regard to the set of signals they
are defining and placed at the signal definitions or near the logic
that use them. To spread out the conditions of a property invites
misconception and information hiding - things that assertions
are trying to prevent.
>Well there are many things that can fall in this category. We recognize the
>fact that it will not be prudent to limit the expressivity of assertions to
>only that set, which can be EFFICIENTLY verified by formal techniques. Some
>examples of these would be "retriggerability" of assertions, very
>deep/unbounded temporal specifications, multi-nested regular expressions
I think it would better to provide a well thought out model for
assertion
operations, rather than a general solution that provides for almost
anything
and the confusion that results. Assertions are best when they are small
and written for a specific cause. For the cases of writing assumptions
to direct stimulus, there may be cases where it is better to use a
general
modeling language rather than trying to add elements to control and
direct
a temporal regular expression by retriggering, stalling, etc. We already
have Verilog (SystemVerilog) as a general language. The problem [using
verilog for assertions] is that the language is too general and the
resulting solutions too verbose to easily convey the intention and
expectations originally conceived.
Can you give a specific example (like you did with the FSM example)
where
it is useful to have a property/assertion that requires something not
considered efficient in a formal setting, but is efficient and requires
more complex controls in a simulation setting.
Thanks Rajeev;
This archive was generated by hypermail 2b28 : Tue Jul 30 2002 - 10:13:46 PDT