Subject: Re: Assertion requirements
From: Adam Krolnik (krolnik@lsil.com)
Date: Wed Jul 31 2002 - 15:10:54 PDT
Good afternoon all;
I would like to add a final set of requirements. These will be numbered
where I left off.
#11. Formal definitions of the assertion semantics shall be delivered
with the Assertion LRM to the full Accelera committee.
Justification:
Formal definitions provide basis for formal analysis tools to
properly utilize the assertion semantics in their tools without
qualification as to correctness.
The formal definitions also provide a basis for implementation
in simulation semantics. The formal definitions provide the
official definition when corner cases or implementation
deficiencies are present.
Formal definitions allow various implementations to be formally
verified as correct. This provides a closed loop of correctness
by formal verification.
-----------------------------------------------------------------------
#12. Simulation semantics shall be delivered with the Assertion LRM
to the full Accelera committee. These semantics shall be consistent
with the formal definitions (derived from the semantics and
re-expressed in simulation terms.)
An initial list of required semantics should include (but not be
limited to specifying:)
starting point of assertions
pass/ fail point of an assertion
ending time point (if different than pass/fail.)
Operation of assertions with overlapping time ranges.
operation of degenerate cases (expected signal currently occurring,
expression fulfilled in current cycle, etc.)
Justification:
Assertions developed at a simulation level should be equivalent at
a formal analysis level. Assertions developed at a formal analysis
level should be equivalent at a simulation level. Users do not want
to have to translate assertions from a simulation or formal analysis
level to the other level. Translating properties is a barrier to
properly using analysis tools and simulation tools to verify a
design.
An explanation of the correct semantics in the end point/corner cases
provides for better chances of correctness rather than potential
misintepretations.
------------------------------------------------------------------------
#13. Sugar contains the function (like) methods prev(), rose(), fell().
Propose an additional method $stable() and rename rose, fell
to posedge and negedge respectively.
$stable(expr) :== (prev(expr, 1) == expr)
Justification:
With a method to obtain past simulation state, three common
operations
are used: change to 1'b1 (posedge), change to 1'b0 (negedge) and
no change (stable.) These three can be defined as follows:
$posedge(bit) :== ! $prev(bit, 1) & bit
$negedge(bit) :== $prev(bit, 1) & !bit
$stable(expr) :== $prev(expr, 1) == expr
------------------------------------------------------------------------
#14. Extend $isunknown(), $onehot(), $onehot0() to allow for multiple
signals.
E.g.
$isunknown(a,b,c) instead of $isunknown({a, b, c})
$onehot(a,b,c) instead of $onehot({a, b, c})
$onehot0(a,b,c) instead of $onehot0({a, b, c})
Justification:
Ease of use - concatenating the arguments is not necessary.
A function can accpet multiple arguments and work fine.
Thanks.
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
This archive was generated by hypermail 2b28 : Wed Jul 31 2002 - 16:26:32 PDT