Subject: [sv-ac] Clarification of sequence implication with first_match.
From: Adam Krolnik (krolnik@lsil.com)
Date: Mon Apr 21 2003 - 13:52:34 PDT
Hello all;
In section 17.10 it describes properties and the results of property evaluations.
I would like to propose this clarification to section 17.7.11, which describes
implication. This change clarifies the discussion in 17.10 for the implication
operation that it references.
Comments?
Adam Krolnik
Verification Mgr.
LSI Logic Corp.
Plano TX. 75074
Section 17.7.11, pg 176.
Proposed [Addition]:
Add bullet to list after "The following points should be noted for |-> implication:"
o seq1 |-> seq2 is equivalent to seq1 |-> $first_match(seq2)
Justification:
On page 188(pg 195 of pdf) the second paragraph speaks about implicit transformations
by addition on $first_match() to a sequence expression. It continues that implication
semantics apply for implications...
In the bullet list describing notes for the overlapping implication operator, it
describes several facts about implication. The conclusion of these facts is
that a |-> b is equivalent to a |-> $first_match(b). Thus I recommend
the clarification of this as supporting the discussion in 17.10
This archive was generated by hypermail 2b28 : Mon Apr 21 2003 - 13:54:38 PDT