Subject: Re: Assertion requirements
From: Simon Davidmann (simond@co-design.com)
Date: Fri Jul 12 2002 - 08:01:01 PDT
Adam
It seems like these requests are all about extending and modifying Sugar.
You have sent this to the wrong committee - if you want to modify Sugar -
then you need to address this to the Formal Committee - they are the ones
that are working to modify Sugar as a standard property language.
This committee is about extending SystemVerilog DAS.
Simon
At 02:42 PM 7/11/2002, Adam Krolnik wrote:
>Good afternoon;
>
>Here is an initial list of requirements I would like to see.
>
>---------------------------------------------------------------------------
>#1 Add Sugar_Declaration and Verification_Directive (Sugar 2.0
> Grammar productions) as an element of module_item and interface item
> (SystemVerilog 3.0 grammar productions.) All productions downward
> from the Sugar 2.0 productions shall be added to support the grammar.
>
>Justification:
> Regardless of whether or not a given property is simulatable,
>properties
> are best kept with the design source code.
> They are not forgotten.
> They are more readily kept up to date with the source code.
> They are not lost.
> They transport very easily in the source code to other places.
> All tools can see them coupled with the relevant code.
> RTL may be created from a file with properties already in them.
> ETC.
> An interface definition is a great place to put assertions/properties
> to further explain how the interface is to be used and ensure that it
> is used in the desired manner.
>
>Problems with this requirement:
> Some properties can not be supported in a simulation environment.
> There may be some minor syntax differences between Sugar and Verilog,
> that would be trivial to ammend.
> The entire Sugar grammar is not necessary at the RTL level, now. But
> more accomplished people will use the entire grammar.
>
>
>---------------------------------------------------------------------------
>#2 Provide a method to disable Sugar verification directives
>(properties)
> separate from the property declarations/directives. Properties not
>disabled
> shall be considered supported. Properties not supported shall produce
> a compilation (or at the beginning of simulation - but not dynamic)
> error indicating nonsupport. Properties disabled shall be ignored
> (but compiled) by the tool. Properties relying on unsupported
>properties
> shall also produce an error indicating nonsupport.
>
> The method of disabling Sugar verification directives shall allow for
> multiple tools.
>
>Justification:
> A. Some properties can not be support in a simulation environment.
> B. Commenting properties out does not provide support for other tools
> that do support such properties. Different tools may support
>different
> sets of properties.
> C. A given tool's implementation of a property may contain errors.
>Different
> tools will support a given property.
> D. A property may be written twice in two forms (due to C.) Different
>tools
> would want to use one, not both.
>
>Problems with requirement:
> This could be difficult!
> Maybe there should be support to override a verification directive
>(e.g.
> switch assert to assume) and there should be a new verification
> directive to disable a property.
> How do you provide support for a particular tool? Attributes ... ?
>
>---------------------------------------------------------------------------
>#3 Extend Sugar Verification directives to support the systemVerilog
> merged grammar:
> <Verification Directive > <pass statement> else <fail statement> ;
>
> This allows Sugar 2.0 Verification directives to include pass/fail
> statements for simulation operations.
>
>Justification:
> Assertions shall be capable of reporting a customized message with a
> controllable severity.
>
>Problems with this requirement:
> Non simulation tools would have to ignore these verilog statement.
>
>---------------------------------------------------------------------------
>#4 Sugar Verification directives shall be simulated using assert_strobe
> semantics - they should simulate at the end of the timestep.
>
>Justification:
> Combinatorial logic values are not stable until the end of a timestep.
> Therefore a property that uses combinatorial logic (or nonblocking
>assigned
> register) will not operate with the correct signal values. This does
>not
> remove the possibility of failing a property with an incorrect signal
>value.
> Signals may arrive in a later timestep due to the use of modeled
>delays in the
> simulator. Properties in this environment would need to be run
>(clocked)
> with a delayed clock.
>
>Problems with this requirement:
> The systemVerilog assert statement does not use strobe semantics -
>there could be
> confusion if both exist. Propose an addition to add modeling delay to
> clock specification?
>
>
>--------------------------------------------------------------------------
>#5 Extend Sugar 2.0 prev() function to support bit vectors.
>
>Justification:
> {prev(a[2], 2), prev(a[1], 2), prev(a[0], 2)} === prev(a[2:0], 2)
>
> There is no reason to require a user to expand bit vectors to access
>previous
> values of a signal. This would be an impedement to usage.
>
>Problems with this requirement:
> Is there a reason Sugar does not support this?
>
>--------------------------------------------------------------------------
>#6 Extend Sugar to support overlapping properties with fifo semantics
> on positive directives (not including never directives)
> (so the user does not have to model fifo semantics [incorrectly].)
>
> This means that a property like "assert always req -> {[*1:10]; ack}"
>could
> be used safely instead of requiring fifo modeling to ensure that two
>req's
> don't use the same ack as a completion event.
>
>Justification:
> In many of the examples from the FVTC there was little mention of
>overlap
> in the antecedents. In the Sugar 2.0 tutorial there is no
>consideration of
> overlapping antecedents (with the consequent sequences.) This is a
>trap
> waiting to spring on users. The above property can work for several
>waveforms
> and appear to be fine. But when events begin to occur with
>variablility, it
> will produce false positives.
>
>Problems with this requirement:
> This is an enhancement to Sugar 2.0, not systemVerilog.
>
>--------------------------------------------------------------------------
>#7. Replace systemVerilog temporal expressions in assertions with Sugar
> Temporal_Expression (grammar production.)
> This will provide compatibility between Sugar properties that exist a
>declarative
> elements, and systemVerilog assertions that can be procedural.
>
>Justification:
> Why support two temporal expression definitions. One is far richer and
>more well
> defined.
>
>Problems with this requirement:
> This is not compatible with SystemVerilog 3.0. This though is a spec
>that has
> only been out for a month (and will only be out for 6-8 months before
>superseeded.
>
> Sugar temporal expressions also include components not supportable in
>a simulation
> environment.
>
>--------------------------------------------------------------------------
>#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.e. The simulator should rewrite a given procedural assertion as a
>declarative
> assertion proceeded by the composition of variables tested by
>if/case
> statements as an antecedent.
> E.g.
>
> always_comb // assert_prob_1
> begin
> case (next_state)
> A: begin
> case (theinputs)
> I1: if (!thecounter)
> begin
> theout = these_inputs & these_states;
> good_st: assert_strobe ({1;$inset({the_st, the_st2}, 2,
>3)}) @@(posedge clk)
> else $error("We are doing the wrong thing! state=%h,
>inps = %h\n",
> state, {in1, in2, in3});
> ...
>
> This assertion shall be implemented as if it was written as:
>
> always @(posedge clk)
> // Run at the end of the timestep (i.e. strobe semantics.)
> #(1-) if ( next_state == A // from case statement
> && theinputs == I1 // from the next one.
> && !thecounter // from the it
> ) assert_strobe ({1;$inset({the_st, the_st2}, 2, 3)})
>@@(posedge clk)
> else $error("We are doing the wrong thing! state=%h, inps =
>%h\n",
> state, {in1, in2, in3});
>
>Justification:
> The example above may fail falsely due to ordering of the variables
>changing.
> If next_state changes late in the timestep, the assertion should not
>even
> be started.
>
> There is a way to ensure that this assertion works correctly. As Harry
>points out
> the addition of disable good_st at the beginning of the block would
>prevent
> false firings. E.g.
>
> always_comb // assert_prob_1
> begin
> disable good_st;
>
> Of course one needs to remember to always add a disable for each
>assertion statement
> put into a combinatorial block. This may be a ways away from the
>actual statement,
> and is easily overlooked (in other words, dangerous stuctures.)
>
> This fix though does not allow one to have overlapping assertion
>sequences since
> the disable statement stops threads of the statement.
>
> Thus, I recommend this requirement to save us from all this headache.
>
>Problems with this requirement:
> It makes the implementation a little more difficult.
> It is different from SystemVerilog 3.0
>
>--------------------------------------------------------------------------
>#9. Extend sugar Verification directives to include optional clocking
> specification (to override the presumed global clocking signal.)
> Include systemVerilog optional name for directives too. Suggested
> syntax includes:
>
> <name> : assert always @(posedge clk) <Expression> ...
>
>Justification:
> It appears that a default clock can be specified for subsequent
>properties.
> I presume that formal tools require the user to define the clock and
>properties
> use that. Simulation needs to specify the clock a little more
>explicitly.
> One may want to set a default clock for a module/interface for all
>properties.
> And one may want to specify a clock on a particular property for only
>that
> property.
>
>Problems with this requirement:
> Optional clock is embedded within the Sugar grammar.
> Naming properties/assertions may already be supported by Sugar
>(where?)
>
>--------------------------------------------------------------------------
>#10. Require the systemVerilog name for directives/properties to be
>mandatory.
>
>Justification:
> It is good methodology to name properties/assertions/coverage, etc.
>The name
> provides a symbol to talk about and refer to in discussions/reports,
>etc.
> Without a name, one is left with a number or a line number. When you
>have
> many properties in a module, having a name prevents you from looking
>at
> the wrong property when it fails. Often without a name, people can
>find the
> wrong assertion/property to review.
>
>
>Problems with this requirement:
> Currently it is optional.
>
>--------------------------------------------------------------------------
>
> Thanks.
>
> Adam Krolnik
> Verification Mgr.
> LSI Logic Corp.
> Plano TX. 75074
This archive was generated by hypermail 2b28 : Fri Jul 12 2002 - 08:24:22 PDT