RE: [sv-ac] FW: [ovl-vsva] Property library enhancements

Shalom,
 
Dimitry's comments are very interesting. We have been trying to resume the commitee for discussion of open items. These are items of equal importance. Can intel become more active in this commitee? Can intel also make a request for this commitee to start again?
 
Thanks
 

Hillel Miller>

 

  _____  

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Bresticker, Shalom
Sent: Wednesday, November 30, 2005 12:33 PM
To: sv-ac@eda.org
Subject: [sv-ac] FW: [ovl-vsva] Property library enhancements



I think this should interest the entire group.

There has been subsequent correspondence, but I think you have to access to the Members area of the Accellera web site in order to see the mail archives.

 

Shalom

 

  _____  

From: Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com] 
Sent: Tuesday, November 29, 2005 5:53 PM
To: ovl-vsva@lists.accellera.org
Subject: [ovl-vsva] Property library enhancements

 

Hi all,

 

We see several problems with OVL, which prevents most of leading Intel projects from using it. The most important problems are: 

*	Redundant verbosity   

*	Lack of context sensitivity 

*	Limited expressiveness 

*	Efficiency for the formal verification flow 

*	Compatibility between different OVL implementations. 

 

I think that one of the goals of our subcommittee is to define a property library standard which would answer the needs of the users and would increase the productivity of designers and validators. Some of the features will require making enhancements in SystemVerilog, and the cooperation with the SystemVerilog committee will be needed.

 

My recommendation is to change the committee goal from being OVL centric to be:

Define a standard property library that can be embedded natively in the RTL context.

 

I am briefly describing below the main issues, most of them I have already sent in my previous mails.

 

Context Sensitivity

 

OVL is not context sensitive

 

SVA is context sensitive:

*	The property clock is inferred from the procedural block or from the default clocking 

*	The property antecedent is inferred from the current condition 

 

E.g., in the following fragment

 

always_ff @(posedge clk iff reset == 0 or posedge reset)

      if (reset)

            s <= 0;

      else begin

            s <= s + 1;

            p: assert property (s < 1b'111);

      end

 

the property p is equivalent to the standalone property

 

assert property (@(posedge clk)) !reset |-> s < 1b'111;

 

Note that there is no context sensitivity support in OVL. Even when OVL is built on top of SVA, since all OVL properties are module instantiations, and the modules cannot be instantiated inside procedural blocks, the context sensitivity is completely lost.

 

OVL cannot be used inside interfaces

 

Let alone the fact that OVL cannot be used inside the interfaces since the interfaces cannot contain module instantiations. This is a serious drawback because the interface is a natural place to put the properties there.

 

OVL is too verbose

 

OVL properties are too verbose and non-intuitive. E.g., the following OVL checker

 

assert_delta

    #(OVL_ERROR, 16, 0, 8, OVL_ASSERT, "Error: y values not smooth", OVL_COVER_ALL)

    valid_smooth ( clk, reset_n, y );

 

means that if the difference between the value of y at each rising edge of clk and the new value (i.e., the delta value) is in the range from 0 to 8, inclusive.

 

It would be much more intuitive to write instead (using standard SystemVerilog notation)

 

assert_delta(.msg("Error: y values not smooth"), .val(y), .max(8));

 

using default values for the clock and the reset signals.

 

 

SVA Metalanguage

 

SV(A) has its own inherent metalanguage problems which prevent building a user-friendly property library.

 

SVA does not have a good encapsulation mechanism for properties

 

Unfortunately, property and sequence template cannot be used instead of modules or interfaces since several properties cannot be incorporated into the same block. More than that, sometimes RTL code is also provided along with the SVA properties, see assert_frame_logic for an example.

 

Missing SVA features

 

Most of the above and related issues cannot be resolved using existing SystemVerilog and SVA apparatus, and several enhancements in the language itself are needed:

 

*	Ability to specify macros with default parameters and passing parameters by name 

*	Ability to specify default global clocking and default global reset signal 

*	Ability to instantiate property wrappers inside the procedural code and inside an interface. These wrappers should be able to accept sequence and property templates 

*	Ability to write concurrent assertions inside for loops with the bounds known at the compilation time. This should unroll the assertions as done by generate for loops 

*	Ability to use property wrappers for immediate assertions also 

 

 

Formal Verification

 

Liveness cannot be expressed

 

The OVL checkers can express only safety properties. General form liveness properties cannot be synthesized into RTL code, therefore the Verilog implementation of liveness properties cannot be written at all.

 

SVA is targeted for dynamic validation

 

SVA itself needs also to be enhanced to respond the formal verification needs. It is very important that the same checkers run in the formal verification, the dynamic validation and the hybrid environments.

 

Missing SVA features

 

Here are some of the features missing in SVA:

*	LTL operators are missing. One should use sophisticated workarounds to implement them. Thus, even to implement a plain globally operator, a recursive property should be written. eventually globally a; should be written as not(##[0:$] a |-> ##[0:$] !a). 

*	Some properties have to be split into two - a one time part should be specified as a different property inside an initial block, and the continuous part should be specified outside of an initial block. Thus a property saying that the clock has a pattern (01)* has to be split into two:
initial assert property (clk = 0);
assert property (clk |=> !clk);
which is inconvenient. 

*	No system clock is available - there is no way to specify in SystemVerilog a default clock such that all events happen at the ticks of this clock. The implicit system clock is important to specify stability templates. Inability to express the system clock also has a negative impact to FV performance. 

*	No next values of signal and variables. In the model checker data model each variable is represented as a pair of the current and the next value. Ability to specify next values improves the model checker performance since it eliminates needs in the new variables. 

*	No support for the high level modeling - restricted free variables are missing. X values are not a solution 

*	Local variable semantics is not suited well for the formal verification 

 

Most of the missing SVA features could be taken from PSL.

  

Thanks,

Dmitry