A Community of Verification Professionals

Create an Account	Home | Calendar | Downloads | FAQ | Links | Site Admin | Your Account
Login Nickname Password Security Code: Type Security Code BACKWARD Don't have an account yet? You can create one. As a registered user you have some advantages like theme manager, comments configuration and post comments with your name. Modules · Home · Downloads · FAQ · Feedback · Recommend Us · Web Links · Your Account Advertising Who's Online There are currently, 50 guest(s) and 0 member(s) that are online. You are Anonymous user. You can register for free by clicking here    Verification Guild: Forums  Forum FAQ   Search   Usergroups   Profile  Digest    Log in  Type-Checking SVA Parameters Goto page Previous  1, 2          Verification Guild Forum Index -> Assertions View previous topic :: View next topic   Author Message vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1237 Location: Los Angeles, CA Posted: Thu Jun 17, 2004 8:23 pm    Post subject: Bernard, You're correct, a LIFO would satisfy the property that I described. Thus, by itself is not sufficient to describe a FIFO. Mike, Thanks for your clarification on using a parameter to set a value for an upper range. Quote: For example, there supposedly exist methods to translate SVA into PSL. If so, then they must have to transform away cases like this somehow, or are local variables not translated? PSL 1.1 does not support the concept of local variables. They have to be emulated at the modeling layer // not an easy thing to do. That is an interesting thread. Ben _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1237 Location: Los Angeles, CA Posted: Thu Jun 17, 2004 8:40 pm    Post subject: Quote: Section 17.6 Declaring Sequences ...A sequence can be declared with optional formal arguments... An actual argument can replace an: -Identifier -Expression -Event control expression -upper range as $ The LRM is not clear on what an argument of a property can replace. One can assume that it's the same as the sequences. A search on "upper range as $" or "actual argument can replace" yield one result. Anyone with insights? _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Fri Jun 18, 2004 12:13 pm    Post subject: Mike, I looked at Appendix H again, and I confess I'm *NOT* the worlds expert on abstract math, but I can't see anything that precludes the type of assignment issues I mentioned. I'm thinking of things like: !strb [*] ##1 ((( !strbA && !strB, value = portA )[*] ##1 strbA && !strB) or (( !strbA && !strbB, value = portB )[*] ##1 !strbA && strB)) Forgive me for any syntax errors - I promise I'm better with PSL! The problem to my mind is what ends up in the variable "value" in the event strA becomes active? Should the engine: 1) blindly assign both portA and portB every clock during which !strbA && !strB. presumably some engines will then favour portA over portB, and others vice versa, creating problems akin to the old verilog race hazards 2) does it have to be smart enough to work out what the user REALLY wanted to do 3) is this actually illegal, in which case how do we recognize the fact Incidentally, I can see a MILLION ways to write this fragment to avoid the problem - my question is how the heck does a tool builder cope with users (perhaps inadvertently!) coding in this way? Regards Bernard Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Fri Jun 18, 2004 3:11 pm    Post subject: Hi all, I checked with Erich Marschner, and he pointed to page 227 of the SVA 3.1a LRM. Specifically, item 3) which says "Each thread for an operand of an or that matches its operand sequence continues as a separate thread, carrying with it its own latest assignments to the local variables that flow out of the composite sequence. These threads do not have to have consistent valuations for the local variables." Translated, that seems to imply that in my example the compiler should do what the user expects. Also Erich pointed out that if both paths complete (which is possible in my case) the assignment to the variable is indeterminate! See the para starting "There are special considerations...." Ouch! Regards Bernard Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1237 Location: Los Angeles, CA Posted: Tue Jun 29, 2004 8:13 am    Post subject: Quote: LRM Section 17.6 Declaring Sequences ...A sequence can be declared with optional formal arguments... .. -upper range as $ Can the delay range be dynamic using a variable, like ##[5:w] My thoughts: NO. The range must be known at compile time, like ##[0:5], or ##[0:$] " ... based on 17.6 " This actually seems to be saying that you the answer is YES, since I could have written a $ for the upper range in my example. From a discussion with John Havlice in sv-ac, the range has to be static . . From the perspective of the formal semantics, local variables cannot influence the endpoints of temporal ranges ** That makes sense since the sequence_instance.ended cannot be dynamically changed, as with the case of a variable used in the range (a variable can be changed within the sequence). I made the recommendation that 2. LRM Section 17.6 Declaring Sequences ...A sequence can be declared with optional formal arguments... .. -upper range as $ TO: -upper range as $ or a static natural number. Ben _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top MikeP Junior Joined: Jun 15, 2004 Posts: 5 Location: Waltham, MA Posted: Tue Jun 29, 2004 11:24 am    Post subject: Thanks Ben, Someone else pointed me at that discussion and I'm trying to get on the mailing list. I still have one other concern remaining. You can post it if I don't get on the mailing list by tomorrow. Since local vars can be used as any expression, it seems that they can be used as array accessors. This would seem to present the possibility for dynamic array-out-of-bounds errors. Is this legal or not? Thanks, MikeP Bluespec, Inc Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1237 Location: Los Angeles, CA Posted: Tue Jun 29, 2004 12:36 pm    Post subject: Quote: Since local vars can be used as any expression, it seems that they can be used as array accessors. This would seem to present the possibility for dynamic array-out-of-bounds errors. Is this legal or not? I believe that you'll get a runtime error, just like you do in VHDL. A related answer to a similar question: Quote: > 2. What happens if the range is a downward range, like [10: 3} or even > a negative range, like [-3: 5], [-3: -10], [-10: -4]? Is that > considered a "null" range a la VHDL? > > Or, is this totally illegal, and a runtime error would occur? Regarding descending temporal ranges, these are also not given any formal semantics. Therefore, they should result in compile-time errors. A local variable can be used as a bit selector or as the base of a variable part selector. Best regards, John H. _________________ Ben Cohen http://www.systemverilog.us/ * SystemVerilog Assertions Handbook, 3rd Edition, 2013 * A Pragmatic Approach to VMM Adoption * Using PSL/SUGAR ... 2nd Edition * Real Chip Design and Verification * Cmpt Design by Example * VHDL books Back to top Display posts from previous: All Posts1 Day7 Days2 Weeks1 Month3 Months6 Months1 Year Oldest FirstNewest First         Verification Guild Forum Index -> Assertions All times are GMT - 5 Hours Goto page Previous  1, 2 Page 2 of 2   Jump to: Select a forum Main----------------MainEDA NewsCommunity Services Networking----------------Looking for a jobLooking for candidates Archives----------------AssertionsCoverageFormalSimulationDesignMiscellaneous Test----------------Test  You can post new topics in this forum You can reply to topics in this forum You cannot edit your posts in this forum You cannot delete your posts in this forum You cannot vote in polls in this forum Forums ©

Verification Guild © 2006 Janick Bergeron
Web site engine's code is Copyright © 2003 by PHP-Nuke. All Rights Reserved. PHP-Nuke is Free Software released under the GNU/GPL license.
Page Generation: 0.507 Seconds