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

Which committee has not started again? Are you referring to OVL or SV-AC?

--- Johny.





Miller Hillel-R53776 <r53776@freescale.com> 
Sent by: owner-sv-ac@eda.org
12/09/2005 09:48 AM

To
"Bresticker, Shalom" <shalom.bresticker@intel.com>, sv-ac@eda.org
cc
Miller Hillel-R53776 <r53776@freescale.com>
Subject
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