[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