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, 47 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 Sequence technique Goto page 1, 2  Next          Verification Guild Forum Index -> Assertions View previous topic :: View next topic   Author Message romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Wed Nov 17, 2004 8:43 pm    Post subject: PSL Sequence technique Is there a general PSL technique used when faced with this situation? If SeqA then either SeqB or SeqC can occur. Where SeqB and SeqC are different lengths. More specifically, I'm trying to handle this generalized case. {a} |-> {b}; or {a} |=> {(~a & ~b)[*];~a & b} If 'a' occurs then 'b' is either on the same cycle or on a future cycle before another 'a'. Thanks. Last edited by romi on Wed Nov 17, 2004 10:08 pm; edited 1 time in total Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Wed Nov 17, 2004 10:07 pm    Post subject: I think my specific case can be made to work by simplifying it. I already know that when 'a' and 'b' occur at the same time, that is a good case and there is no need to check it. I think the property then becomes this: {a & ~b} |=> {(~a & ~b)[*];~a & b}; However, the question remains for a case like this: {a} |-> {b;c}; or {a} |-> {d;e;f}; Where when 'a' occurs then either {b;c} occures or {d;e;f}; Thanks. Back to top hemanth Senior Joined: Aug 16, 2004 Posts: 93 Location: Bangalore Posted: Thu Nov 18, 2004 12:04 am    Post subject: Romi, this I feel can be tackled using let x = (b or c or d or e or f) then property reqd is {(a & ~x);(~a & ~x))[*]} |=> {{b;c}|{d;e;f}}; I am not very sure of the syntax though. rgds Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1237 Location: Los Angeles, CA Posted: Thu Nov 18, 2004 12:41 am    Post subject: Quote: If 'a' occurs then 'b' is either on the same cycle or on a future cycle before another 'a'. The solution is fairly simple: use the before construct Code: a before_ b: The before!_ and before_ operators are inclusive operators, and specify that the left operand holds before or at the same cycle as the right operand holds. {a} |-> {b before_ a}; If you want b to be before, but not at the same cycle as a then Code: {a} |-> {b before a}; The other proposed solutions look ok, but are not as elegant. Ben Cohen _________________ 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: Thu Nov 18, 2004 3:19 am    Post subject: romi, Quote: If SeqA then either SeqB or SeqC can occur. Where SeqB and SeqC are different lengths. the answer in all cases (whether or not SeqB and SeqC are booleans or complex sequences) is: Code: {SeqA} |-> {SeqB | SeqC} if, as in your simple example, the timing is such that if SeqB occurs it starts the same cycle as SeqA but if SeqC occurs it starts the cycle after SeqA, then you can code Code: {SeqA} |-> {SeqB | { true ; SeqC } } using this general template, your simple example: Quote: If 'a' occurs then 'b' is either on the same cycle or on a future cycle before another 'a'. could be coded as follows: Code: {a} |-> { b | { true ; (~a & ~b)[*] ; ~a & b }} note that in this simple case, there is an easier way: Code:  a -> (b | next (b before a)) or Code:  (a & ~b) -> next (b before a) hemanth, i'm not sure i understand why you think that the definition and use of your signal 'x' is needed. the general solution can be used in this case to get Code:  {a} |-> { {b;c} | {d;e;f} } ben, first, the result of the application of the "before" operator is a property, not a sequence. therefore, you cannot use curly braces on the right-hand side. second, your proposed solution to the simple case does not give the desired result: it gives a formula that holds only when 'a' does not. to see this, consider the case that 'a' holds at cycle 0 (since there is no "always" around your property, cycle 0 is the only "starting" cycle that is relevant). now, at cycle 0, the right-hand side of your formula does not hold ('a' holds immediately, therefore "b before a" does not hold). to fix this, you need to insert a "next" operator before the sub-property on the right-hand side. however, then the property will fail in the case that 'a' holds and 'b' holds immediately, a case which romi wanted to pass. therefore, you need to take care of this case by checking for 'b' the current cycle. putting it all together gives one of the simple solutions using "before" that i presented above. cindy. Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Thu Nov 18, 2004 7:01 am    Post subject: Thanks for the input. I get compile errors with cindy's examples. Code: // psl a_to_b0: assert always ( a -> (b | next (b before a)));                                              | ncvlog: *E,ILLPRI (/test.v,15|45): illegal expression primary [4.2(IEEE)]. // psl a_to_b0: assert always ( a -> (b | next (b before a)));                                                        | ncvlog: *E,EXPRPA (/test.v,15|55): expecting a right parenthesis (')') [4.3][9.7(IEEE)]. // psl a_to_b0: assert always ( a -> (b | next (b before a)));                                                             | ncvlog: *E,ALXSCN (/test.v,15|60): Expected statement terminator ";". // psl a_to_b1: assert always ( {a} |-> { b | { true ; (~a & ~b)[*] ; ~a & b }});                                                    | ncvlog: *E,ILLPRI (/test.v,16|51): illegal expression primary [4.2(IEEE)]. Is there something obvious that I'm missing? Thanks again. Back to top cindy Industry Expert Joined: Aug 17, 2004 Posts: 309 Posted: Thu Nov 18, 2004 7:31 am    Post subject: romi, i don't know why you are seeing a syntax error for the first one. it parses fine in my verilog-flavor psl parser. for the second one, it parses in my parser, but i think perhaps that is a bug, as i don't think "true" is legal in verilog. try replacing "true" with [*1] and see if that works better. cindy. Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Thu Nov 18, 2004 7:34 am    Post subject: Code: // psl a_to_b1: assert always ( {a} |-> { b | { [*1] ; (~a & ~b)[*] ; ~a & b }});                                                  | ncvlog: *E,ILLPRI (/test.v,16|49): illegal expression primary [4.2(IEEE)]. Still gets the same error. So, I should probably report these problems to the vendor. If they are not supporting the syntax, I should get a different error obviously. Thanks. Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Thu Nov 18, 2004 7:38 am    Post subject: Or is is possible that some of this syntax is "new" to the latest PSL and this tool may only know the rules about a previous version? Back to top cindy Industry Expert Joined: Aug 17, 2004 Posts: 309 Posted: Thu Nov 18, 2004 7:40 am    Post subject: romi, just a guess: try putting braces around the [*1], like this: { [*1] }. i think it should parse without them, but this might be an easy workaround. cindy. Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Thu Nov 18, 2004 7:45 am    Post subject: Quote: just a guess: try putting braces around the [*1], like this: { [*1] }. i think it should parse without them, but this might be an easy workaround. Nope, same error. Thanks for the the effort! Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Thu Nov 18, 2004 7:47 am    Post subject: Interestingly, this does not get an error. Code: // psl a_opts: assert always ( {a} |-> { {b;c} | {d;e;f} }); Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Thu Nov 18, 2004 7:48 am    Post subject: I applied your solution to the 'b' instead and it worked: Code: // psl a_to_b1: assert always ( {a} |-> { {b} | { [*1] ; (~a & ~b)[*] ; ~a & b }}); Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Thu Nov 18, 2004 6:10 pm    Post subject: Quote: i don't know why you are seeing a syntax error for the first one. it parses fine in my verilog-flavor psl parser. I used the || instead of the | before the next and the parser took the syntax. Does that seem right? Code: // psl a_to_b0: assert always ( a -> (b | next (b before a))); Code: // psl a_to_b0: assert always ( a -> (b || next (b before a))); Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1237 Location: Los Angeles, CA Posted: Thu Nov 18, 2004 7:03 pm    Post subject: Code:  // psl a_to_b0: assert always ( a -> (next (b before_ a))); This compiles OK in ModelSim. It states that in cycle after 'a', 'b' should occur before or in same cycle as 'a' It uses those property defintions: Code: FL_Property -> FL_Property | FL_Property <-> FL_Property | FL_Property before_ FL_Property Ben Cohen _________________ 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 1, 2  Next Page 1 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.378 Seconds