[sv-ac] Sequential implication proposal

Subject: [sv-ac] Sequential implication proposal
From: dudani@us04.synopsys.com
Date: Tue Feb 04 2003 - 10:13:21 PST

Please provide your feedback for the following sequential proposal:
 
Below is a syntax proposal for making sequential (or boolean) implication a property, thereby allowing it only at the top level. The syntax also allows nesting of implications. 
prop_declaration ::=
        ‘property’ named_prop { ‘,’ named_prop } ;
named_prop ::=
        identifier [ ‘(’ identifier { ‘,’ identifier }’ )’] ‘=’ prop_spec
prop_spec ::=   
        [‘initial’] [‘accept’ ‘(’ expression ‘)’ ] [‘never’] clocked_expr
        | identifier [‘(’ expression_list ‘)’]      // identifier must be a property
clocked_expr ::=
         [event_control]   ‘(’ prop_expr ‘)’
prop_expr ::=
             sequence_expr
             | implication
             | ‘(’  prop_expr ‘)’
implication ::=
            sequence_expr  => prop_expr

Intuitive semantics of the implication is as follows:
1) if there is no match for the sequence_expr, then the result is true. It has no length, as it is a property, not a sequence anymore
2) for every match of sequence_expr, prop_expr must be true at the end point of the match

From the above description, prop_expr can be a sequence_expr. The prop_expr results in true, if there is at least one match of sequence_expr, and false, if no match if found.

We can extend this definition to allow dynamic variables on implications.
Surrendra 


**********************************************
Surrendra A. Dudani
Synopsys, Inc.
377 Simarano Drive
Suite 300
Marlboro, MA 01752

Tel:   508-263-8072
Fax:   508-263-8123
email: dudani@synopsys.com
**********************************************

This archive was generated by hypermail 2b28 : Tue Feb 04 2003 - 10:14:06 PST