[sv-ac] proposal for 1734

All:

I have uploaded a proposal for mantis 1734 (incomplete
fix to Annex E in 0805) and also attached it.

This is a minor fix.

Please have a look and send feedback.

J.H.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.

Proposal for Mantis 1734:  Incomplete Fix to Annex E in Mantis 0805

 

The proposal for mantis 0805 moves “disable iff” to the description of top-level properties in Annex E.  However, the proposal fails to change the abstract grammar for assertions in E.2.1 to refer to top-level properties.  The net effect is to eliminate “disable iff” from assertions.  The fix is simply to change “P” to “T” and “Q” to “U” in the abstract grammar for assertions (2 places each). 

 

There are also some minor font mismatch problems that need to be fixed by switching courier italic (or oblique) to roman italic.  And the abstract syntax can be made closer to the actual SVA syntax by adding parentheses around the property expression that follows “assert property”.

 

These changes are in terms of IEEE Std 1800-2005.

 

Annex E.2.1, p. 565.  CHANGE

 

The abstract grammar for assertions is

A ::= always assert property Q             // "always" form

| always @( b ) assert property P  // "always with clock" form

| initial assert property Q                   // "initial" form

| initial @( b ) assert property P // "initial with clock" form

 

TO

 

The abstract grammar for assertions is

A ::= always assert property ( Q U )                   // "always" form

| always @( b b ) assert property ( P T )   // "always with clock" form

| initial assert property ( Q U )                         // "initial" form

| initial @( b b ) assert property ( P T )  // "initial with clock" form

 

[Note to the editor:  b, U, and T are in roman italic font.  The new parentheses are in courier font.]