RE: [sv-ac] Updated proposal for 1995 (concurrent assertions in loops) posted

From: Seligman, Erik <erik.seligman_at_.....>
Date: Fri Dec 07 2007 - 09:54:08 PST
Ed-- in the paragraph above we have the statement "The action blocks are
then executed with the same set of iterator values that caused the
assertion to pass or fail."  Doesn't this prevent the issue you mention?

________________________________

From: Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
Sent: Friday, December 07, 2007 9:44 AM
To: Seligman, Erik; Lisa Piper; sv-ac@eda.org
Cc: Korchemny, Dmitry
Subject: RE: [sv-ac] Updated proposal for 1995 (concurrent assertions in
loops) posted


Hi Erik,

Just noticed something in your example:

a1: assume property (foo[i])

$display("Good foo vector: %d", my_ints[i]);

else $display("Bad foo vector: %d",my_ints[i]);



The (minor) issue I see is that the assume uses the sampled value of
foo[i], while $display of my_inst[i] ises the current value. If that one
is being also updated elsewhere, even using NBA, this may display a
different value that the one used in the sampled foo[i].

Perhaps use $sampled(my_ints[i]) ?

Best regards,

ed




________________________________

        From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf
Of Seligman, Erik
        Sent: Friday, December 07, 2007 12:12 PM
        To: Lisa Piper; sv-ac@eda.org
        Cc: Korchemny, Dmitry
        Subject: [sv-ac] Updated proposal for 1995 (concurrent
assertions in loops) posted
       
       
        
        I added some comments in the coverage section, and a VPI change,
in response to Lisa's concerns. 
        
        
        Erik Seligman

        Formal Verification Architect

        Corporate Design Solutions
        Design Technology and Solutions

        Intel Corporation

               
        M.S. JF4-402                  
        2111 NE 25th Ave
        Hillsboro, OR 97124

               
        Phone:   (503) 712-3134

               
        

        --
        This message has been scanned for viruses and
        dangerous content by MailScanner <http://www.mailscanner.info/>
, and is
        believed to be clean.




-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Fri Dec 7 10:04:32 2007

This archive was generated by hypermail 2.1.8 : Fri Dec 07 2007 - 10:05:35 PST