Re: [$ieee-1850] {a[*0] : b } // No match?

Ben,

The semantics of fusion is well defined in the PSL LRM.

In B.3.1.1.1 it says:

v |== r1 : r2 iff \exists v1, v2 and \ell s.t. v=v1 \ell v2, v1 \ell
|== r1 and \ell v2 |== r2

where \ell is a letter.

Therefore if r1 or r2 is a sequence matched only by the empty word
(e.g. a[*0]) then there would be no \ell satisfying the above. Thus,
no word v will satisfy the fusion.

Regards,
Dana.

On Mon, 6 Dec 2004 13:30:56 -0800, ben cohen <hdlcohen@gmail.com> wrote:
> I found this in:
> http://www.verificationguild.com/modules.php?name=Forums&file=viewtopic&p=2339#2339
>
> An empty sequence is one that does not match over any positive number
> of clocks. The following rules apply
> for concatenating sequences with empty sequences. An empty sequence is
> denoted as empty and a sequence is
> denoted as seq.
> — (empty ##0 seq) does not result in a match
> — (seq ##0 empty) does not result in a match
> — (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq)
> — (seq ##n empty), where n is greater than 0, is equivalent to (seq
> ##(n-1) 'true)
> We have a similar situation in PSL with the fusion operator instead of the ##0.
> I don't believe the PSL LRM defines what happens in such circumstances.
> Consider the sequence {a[*0] : b }
> Fusion is defined as 2 sequences overlapping by one cycle.
> If one of those cycles is empty (i.e., need not exist, then what?
> SVA defines that as a NO MATCH.
> Ben
> --
> --------------------------------------------------------------------------
> Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
> http://www.vhdlcohen.com/ ben@abv-sva.org
> * Co-Author: SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9
> * Co-Author: Using PSL/SUGAR for Formal and Dynamic Verification 2nd
> Edition, 2004, ISBN 0-9705394-6-0
> * Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn
> 0-9705394-2-8
> * Component Design by Example ", 2001 isbn 0-9705394-0-1
> * VHDL Coding Styles and Methodologies, 2nd Edition, 1999 isbn 0-7923-8474-1
> * VHDL Answers to Frequently Asked Questions, 2nd Edition, isbn 0-7923-8115
> ---------------------------------------------------------------------------
>
Received on Mon Dec 6 23:20:42 2004