[sv-ac] SVA enhancement proposal (#1530)l

Hi all,

 

Based on my experience in using SVA in Intel projects and in
implementing OVL checker library on top of SVA, I came to conclusion
that some important enhancements need to be made in SystemVerilog (not
limited to SVA only) in order to make the language ABV and FV friendly.
I am focusing on two language application areas: (standard) checker
libraries and formal verification. I am attaching a set of presentations
describing different enhancements I suggest. Each presentation contains
enhancement motivation, proposal and discussion. I will be glad to hear
your feedback about the proposal. The presented problems may allow
several solutions, therefore I believe that the problem statements are
more important than the suggested solutions themselves, and I am
definitely open to discuss any proposed solution. It is important the
adopted solutions to be consistent and natural. Being consistent is also
important when discussing enhancements and errata. E.g., issue #928 is
closely related to checkers (see Checkers.ppt).

 

The current version of the presentations incorporates feedback that I
got from several people, mostly during internal Intel reviews and from
the OVL committee participants, and I would like to thank all the people
who contributed to these presentations.

 

I had to post the presentations in Mantis (as issue #1530) since the
message grew too big to be distributed via the mailing list.

 

The order of the presentations is as follows:

1.	SVA+ - Overview
2.	CompilerDirectives - Macro-processing
3.	Generate - Extending generate constructs, user-defined compile
time messages and type query
4.	ModulesAndFunctions - Other enhancements in meta-language
5.	CycleBased - Cycle-based design validation support
6.	Temporal - LTL
7.	Modeling - Property modeling
8.	Checkers - Property containers
9.	Immediate - Immediate assertions

 

I've written the presentations from SV-AC point of view, but they are
relevant for all IEEE P1800 subcommittees, mostly for SV-BC.

 

Thanks,

Dmitry