[sv-ac] Discussion: Legal use of .ended in disable iff ?

Hi,
 
I am just in a discussion with Ben on semantic of disable_iff and ".ended".
Can someone jump in.
 
The major questions are:
 
* does the expression after disable_iff needs an event to be evaluated (both of us guess Yes)
* can ".ended" produce an event (Wolfgang guesses No, Ben guesses Yes).
 
Potentially, clarification in the LRM is needed here.
 
Kind regards,
Wolfgang
 
 
 
 
-----Ursprüngliche Nachricht-----
Von: VhdlCohen@aol.com [mailto:VhdlCohen@aol.com]
Gesendet: Donnerstag, 29. April 2004 04:14
An: Ecker Wolfgang (CL DAT TI MF)
Cc: ajeetha@noveldv.com; srinivasan.venkataramanan@intel.com
Betreff: Re: AW: Legal use of .ended in disable iff ?

Wolfgang,
<I guess this is legal but does not work than expected

        * Because the LRM says, that the disable_iff clause can be applied for asynchronous
          reset, the variables in the expression_or_dist expression must be able to trigger the
          evaluation independent from the clock(s) in the property.

Question and rebuttal:
 1. abort_transfer_q.ended is an ".ended" function of a sequence, and is a Boolean signal
     (at least it is in PSL, I am struggling my way thru SVA here). But it is reasonable to
    believe tha a .ended of a sequence is a Boolean signal, and thus can be treated as such, like a
   an asynchronous reset.
 

        
         
        * This in turn makes me again guessing, that in turn an event is required to trigger the
          evaluation.

If ".ended" is a Boolean signal, then it can trigger an evaluation. If look at the sequence

sequence abort_transfer_q;

@(posedge clk) $rose(mode==BUS_ACCESS) ##1 abort_xfr ;

endsequence

 then the signal abort_transfer_q.ended would be true one cycle after mode == BUS_ACCESS, provided abort_xfr signal occured in that last cycle. I see a "pulse" or even there.

 
* Furthermore I guess, that ".ended" returns a value but not an event.
True. But "disable iff (reset_n) " expects an expression, like reset==1'b1 or simply "reset".
 
LRM
disable iff ( expression_or_dist ) ]
expression_or_dist ::= expression [ dist { dist_list } ]
 
<So, summarizing my guesses, it won't work as intended and the SV-LRM might need some clarification here.>
I see a lot of value in having an "abort" evaluation of property. The use of sequences with ".ended" is very powerful because you can do things like:
  property X;
   disable iff (seq1.ended || seq2.ended || seq3.ended)
    ....
   endproperty : X
seq1, seq2, seq3 are sequences that represents conditions that disables the property.
I really see no reason as to why it would not work, since the disable ifff expects an expression, and a .ended of a sequence is a signal.
 
Ruminating a bit, if seq.ended is a value returned by a function instead of a "signal", then I am not sure if
"disable iff (seq.ended) " would work!
Do you know the answer?
 
By the way, I am a member of Synopsys SystemVerilog Catalyst Program <http://www.synopsys.com/partners/systemverilog/systemverilog_program.html>
http://www.systemverilog.org/products/products_solu.html (see VhdlCohen at bottom)
and we're in the process of "translating" our PSL book to an SVA book. Of course, we're running into issues between the 2 languages, and this is one of them.
 
Thanks for your effort. Please clarify for us the nature of a seq.ended object: a signal that can be used in a "disable iff (seq.ended)" or simply a value or variable with no "timing" associated with it.
Thanks again,
Ben
 

         
         
        By the way, what is the semantic of "abort"?
         
        Wolfgang
         
         
         
         

                -----Ursprüngliche Nachricht-----
                Von: VhdlCohen@aol.com [mailto:VhdlCohen@aol.com]
                Gesendet: Sonntag, 25. April 2004 23:24
                An: Ecker Wolfgang (CL DAT TI MF)
                Cc: ajeetha@noveldv.com; srinivasan.venkataramanan@intel.com
                Betreff: SVA: Legal use of .ended in disable iff ?
                
                
                

                Is this legal? If .ended is a Boolean , it probably is legal.

                This might be a way to provide an abort a la PSL.

                sequence abort_transfer_q;

                @(posedge clk) $rose(mode==BUS_ACCESS) ##1 abort_xfr ;

                endsequence

                property test;

                @ (posedge clk) disable iff (abort_transfer_q.ended)

                     req |=> ##[0:5] ack ##1 bus_ready ##1 data_enb[*32];

                endproperty : test

 
-----------------------------------------------------------------------------
Ben Cohen Trainer, Consultant, Publisher (310) 721-4830
http://www.vhdlcohen.com/ <http://www.vhdlcohen.com/> vhdlcohen@aol.com
Author of following textbooks:
* 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 Wed Apr 28 19:24:50 2004