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, 51 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  PSL Problem 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: 1240 Location: Los Angeles, CA Posted: Thu Sep 16, 2004 10:53 am    Post subject: Cindy, Good response! Now some rebuttal and comments. 1. SVA has addressed the issue of multiple matches by provide a "first_match" function that a user can use to restrict a first match of a sequence. . 2. Section 17.8 of the SystemVerilog LRM identifies rules in using variables, and problematic cases like the one you mentioned are illegal. 3. I like to think of a local assertion variable as a tag local to a thread to be used later for comparisons, as demonstrated in the example in this thread. This is probably the most likely use of an assertion variable. 4. However, if you give an engineer a feature, he'll find ways to apply that feature in many different ways. For example, one can use the local variable in a thread as a counter, resettable under some conditions to characterize a property. 5. Unlike SVA, PSL does not have a "first_match" function. Considering your example, modified slightly: Code: always ({ req; !ready[*] ; go } |=> {bus_enb ; parity_enb ; done }) a non first match of the antecedent will give me an error with the following sequence: cy1 req; cy2 !ready; cy3 !ready && go; // first_match of antecedent cy4 go & bus_enb // 2nd match of antecedent cy5 !bus_enb && parity_enb // fail on 2nd match sub-thread cy6 done // pass on 1st match sub-thread (is sub-thead a good name?) How can we restrict a sequence to a 1st match in PSL? I don't recall this being addressed in the LRM. Thanks, 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 cindy Industry Expert Joined: Aug 17, 2004 Posts: 309 Posted: Fri Sep 17, 2004 5:17 am    Post subject: ben, Quote: Now some rebuttal and comments. i was addressing your comment that it would be not much of a big deal to add dynamic variables to psl. i am not interested in starting a debate on the merits of sva vs. psl. Quote: PSL does not have a "first_match" function. Considering your example, modified slightly: Code: Code: always ({ req; !ready[*] ; go } |=> {bus_enb ; parity_enb ; done }) a non first match of the antecedent will give me an error with the following sequence: cy1 req; cy2 !ready; cy3 !ready && go; // first_match of antecedent cy4 go & bus_enb // 2nd match of antecedent cy5 !bus_enb && parity_enb // fail on 2nd match sub-thread cy6 done // pass on 1st match sub-thread (is sub-thead a good name?) How can we restrict a sequence to a 1st match in PSL? I don't recall this being addressed in the LRM. in this particular case, you can code: Code: always ({ req; (!ready & !go)[*] ; go } |=> {bus_enb ; parity_enb ; done }) cindy. Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1240 Location: Los Angeles, CA Posted: Fri Sep 17, 2004 8:44 am    Post subject: CIndy, I am also not interest in debating a comparison between the two as each has each values in its own niche. From a language standpoint, on the first match issue, a user needs to code the antecedant in a manner to guarantee a first match, as you clearly demonstrated in the example. Thanks, 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 tblackmore Senior Joined: Jan 23, 2004 Posts: 43 Location: Bristol, England Posted: Mon Sep 20, 2004 4:16 am    Post subject: Quote: I am also not interest in debating a comparison between the two as each has each values in its own niche. My understanding was that both SVA and PSL had mainly similar uses, namely to express properties that can be checked against RTL behaviour both dynamically and formally. At least this is how we foresaw using them in the first place. Are the difference niches to which these languages are suited generally accepted? If so, could someone say what they are? Without debating a comparsion between languages if this is undesirable. Certainly without going into the minutiae of each language, which wouldn't be informative. Editor's note: This thread continues in this topic Back to top chrisw Junior Joined: Jan 07, 2004 Posts: 5 Posted: Tue Sep 21, 2004 1:21 pm    Post subject: Quote: Quote: OK, then, can you explain how the your SBE assertion is translated using your tool? Is it done by introducing dynamic variables? sorry, but i am not at liberty to give details of our implementation. in general, i can say that it involves creating checkers on an as needed basis. i also need to note that we have a patent pending on the method. I am concerned about this statement. I think the idea of having a standard language is to allow multiple vendors to provide tools that are compatible, making it easier for users to switch vendors if need be. The key to this is an open standard. What you are saying is that the translation process is closed. However, as you have pointed out, the translation process must be efficient, otherwise the user will derive no benefit. Making the translation process closed forces every vendor to have to invent their own translation algorithms, made more difficult by needing to avoid IBM and other patents.The translation process has no value to the user, it's like the compile phase of a simulator. Therefore, companies will be forced to spend a lot of time and effort developing translators which will not make any money for them. I think the effect of this will be to hinder PSL adoption by making it more difficult for vendors to produce tools, especially startups where the most useful tools are more likely to come from. I suggest the translation process be made open some how. This can either be directly, by making it part of the standard, or by forcing vendors to make their translators open-source and freely licensable. Back to top cindy Industry Expert Joined: Aug 17, 2004 Posts: 309 Posted: Sun Oct 17, 2004 8:02 am    Post subject: back in september, chrisw asked: Quote: In general, are all properties with forall constructs translated by introducing dynamic variables? i can answer the general question regarding what we know how to do. i cannot answer the theoretical question as to what it is possible or not possible to do. in other words, perhaps there are things that are doable that we do not currently do. first, i want to clarify that we do not "translate a forall to a dynamic variable". rather, we have an efficient implementation of forall that in many cases could be used as well for the efficient implementation of dynamic variables. finally, to answer the question: when the 1st reference (temporally) to a forall variable is a comparison in which the forall variable appears alone on the lhs or rhs of the comparison, we have an efficient implementation which could be used as well to implement the equivalent property expressed with dynamic variables. Quote: Under what circumstances is it not possible to translate a forall to a dynamic variable? kirloy gave an example on another thread. i cannot think of an equivalent using dynamic variables for the following property: Code: forall m in {0:30}:  always (a[m] -> next (addresss==m)); cindy. Back to top edcerny Senior Joined: Jan 12, 2004 Posts: 55 Location: Marlborough, MA Posted: Sun Oct 17, 2004 8:20 pm    Post subject: dynamic variable and for all I think that one way to write the PSL property Code: forall m in {0:30}:  always (a[m] -> next (addresss==m)); using local variable in SVA could be as follows (generating one property) Code: genvar i; generate   for (i=0; i<=30; i++) begin : get_all     if (i == 0) begin       sequence s(m);         (a[0], m=i);       endsequence     end     else begin       sequence s(m);         (a[i], m=i) or get_all[i-1].s(m);       endsequence   end : get_all   property p;     int v;     @(posedge clk)  get_all[30].s(v) |=> address == v;   endproperty   a: assert property (p); It will fail if more than one a[i] is true. (I have not tried to run it yet, though.) --- 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.264 Seconds