I'm a newbie. I want to be able to hold data structures that control how a piece of verification IP behaves when instantiated. I also want to be able to use assertions within that verification IP.

Hence, is it possible to use SVA (System Verilog Assertions), specifically "properties" within a class, or am I limited to using modules if I want to use properties?

If I CAN use SVA within a class, would I be able to measure functional coverage on "properties", even if I don't use covergroups? (I guess thats a tool dependent question?)

OBajaj>>

>> Hence, is it possible to use SVA (System Verilog Assertions), specifically
>> "properties" within a class, or am I limited to using modules if I
>> want to use properties?

Unfortunately NO. You can however use a virtual interface, pass class variables into that interface, have SVA on that interface. We showed this in our SNUG Paper, VMM adoption book etc. (See: www.noveldv.com, www.systemverilog.us for details).

DAVE>>

>> The reason it that most implementations perform some level of synthesis in
>> order to evaluate SVA expressions

Dave - why should language restrict this based on implementation details. For example E allows this nicely and is really quite useful. Whenever I speak to a regular E user here, they stumble upon this issue and find it quite disappointing.

Can this be considered for a future enhancement?

Thanks
Ajeetha, CVC
www.noveldv.com

Ajeetha,

SVA supports static formal verification as well as dynamic simulation, something E users did not have to deal with. The semantics required for formal verification are very similar to synthesis, but by their very 'formal' nature, require much more burden on the implementation to prove their validity. (just take a look at Annex E in the LRM)

Dave,
Thanks, yes I'm aware of that (we used Assertions + Formal in our books). But this can be easily said as "this is not formal compatible" - some thing similar to what PSL calls a simple subset (though that has nothing to do with formal, rather it is for simulation subset).

For instance even in today's SVA I know of formal tools putting restrictions on local variables etc.

So I'm really asking an extension and I don't see why it can't be considered.

Regards
Ajeetha, CVC
www.noveldv.com

I'm not a regular participant of the assertions committee, but I think there is a strong desire to keep those requirements in mind and not create semantics that are not formally verifiable. This is all just software, so the voice of users can certainly change that direction.

Dave

Yes, I agree that its quite disappointing to not be able to use assertions under an Object Oriented context, as restricted by SVA definitions.
Hopefully, this restriction could be relaxed in the future, and the tools be made to detect synthesis exceptions.

I mean, there are ALWAYS going to be synthesis exceptions to language constructs, because we use the same language for the s/w paradigm as we do for h/w modeling. Obviously s/w is not synthesizible as it is not meant to model h/w. If the System Verilog language is made less restrictive, the semantic complexity can be passed on to the backend tools.