"urn:schemas-microsoft-com:office:office">
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 expectedQuestion and rebuttal:
- * 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.
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.
If ".ended" is a Boolean signal, then it can trigger an evaluation. If look at the sequence
- * This in turn makes me again guessing, that in turn an event is required to trigger the
- evaluation.
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.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/ 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
------------------------------------------------------------------------------
This archive was generated by hypermail 2.1.8 : Thu Apr 29 2004 - 07:10:14 PDT