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, 41 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- "How do I..." Goto page Previous  1, 2, 3, 4  Next          Verification Guild Forum Index -> Assertions View previous topic :: View next topic   Author Message vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1239 Location: Los Angeles, CA Posted: Mon May 10, 2004 9:24 am    Post subject: Are you using a default clock? // psl default clock= (posedge clk); // assuming in-line psl Also, your "clock sequence clk_seq = {clk[*3];~clk};" is telling me tht you're using a Cadence formal verification tool. The "clock sequence" is Cadence specific. I used Incisive Static Verifier in our book, and it worked ok. I did not experience this multi-edge clock issue that you are addressing. By the way, below is the vunit taht we used in our book for the Cadence Incisive Static Verifier: Code: //For Verilog, file clk_rst.psl (for Cadence’s Incisive™ Static Verifier) vunit clk_rst (trafficlight) { clock sequence const_clk = { clk; !clk }9 ; property rst_low_first_cycle_then_high = {1'b1} |-> { !reset_n ; reset_n}; property rst_high_after_first_cycle = always {reset_n} |=> {reset_n}; assume rst_low_first_cycle_then_high ; assume rst_high_after_first_cycle; // clk +-----+ +-----+ +-- // | | | | // +-----+ +-----+ // reset_n +------------------- // | // +------------+ } 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 bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Mon May 10, 2004 10:09 am    Post subject: First, my apologies for the mistake in the code I posted on Saturday - Ben's interpretation was correct. I have to admit I have a lot more experience of simulation than formal verification, but I don't think the semantics of PSL in the simple form we're using them here define exactly the relationship of assumed signals to clocks, just that the signal must be setup between the sampling clock edges. I'll try to enquire if any more assumptions are made. As you probably know, you can over-ride the default clock for a single property by adding the clock to the end of the property, for example: always { a } |=> { !c[*] ; c } @ (negedge clk1); One way you may be able to achieve the visualization you require is to selectively include the clock into your property and to sample (assume) it on BOTH edges of the clock, for example: always { (a&&clk1) } |=> { {(!c&&!clk1);(!c&&clk1)}[*] ; (!c&&!clk1);(c&&clk1) } @ (clk1); As you can see, this is cumbersome, but the requirement is now that c should become true between the falling and rising edges of clk1. It still doesn't guarantee the waveform will look exactly the way you understand it, but I think that's a function of the formal model check tool. Regards Bernard Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1239 Location: Los Angeles, CA Posted: Mon May 10, 2004 10:59 am    Post subject: Some Model Checking Expectations and Rules about model checking (those are rules that are applicable in today's technology, and will change as the technology matures): 1. A first and foremost requirement for Model Checking is that designs need to be synthesizable and cycle-based. 2. Single clock designs are better supported by today's tool. On that subject, some vendors are making good progress on handling multi-clock issues. http://www.athdl.com/pdf/Clock_Domain_Datasheet.pdf is a paper on "Clock Domain Visualization and Analysis". Notice that from the paper, it appears to be an "analysis tool", and I have no knowledge on how the tool hndles multi-clock properties in PSL. I would not be suprised if the latest version (or the next version) handles the multi-clock assertions Looking at http://www.safelogic.se/products/safelogicverifier.asp Safelogic states "Supports multiple synchronous clocks.". In any case, thw synchronous single clock case, ONE EDGE, is the best supported case. You need to watch how multiple clocks are exressed in PSL Code: default clock clk = (posedge clk); property TEST = always {a;b} |=> {c;d}; This is equivalent to: property TEST = (always {a;b} |=> {c;d}) @ (posedge clk); However, using the default clock above and    always { a } |=> { !c[*] ; c } @ (negedge clk1); This gets translated to: "always" checked at the default clk {a} checked at the default clk { !c[*] ; c } @ (negedge clk1) If you want everything at negedge of clk1, then:    (always { a } |=> { !c[*] ; c }) @ (negedge clk1); Bottom line, you need to understand both your goals and the limitations of the tools that you're using. I, and others in this forum, enjoy commenting and discussing verification issues ... that's the purpose of this forum. However, keep in mind that your formal verification vendor should provide good support .. otherwise he is failing you! 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 romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Mon May 10, 2004 2:43 pm    Post subject: Thanks for the input. I am using the Cadence tool, but not it's most up to date version containing the Black Tie technology. I hesitated to mention the tool name because I didn't know if I should be mentioning specific tools on this site. But anyway... I still get problems with the tool I'm using with the code that has been suggested. However, I may put off my investigation until I can move up to the new tool. It seems like it may be beneficial for others to formally verify the 3 properties of the simple module below instead of me posting my examples of what is not working. Let me know what you think should work and try it if you can. Going through this exercise seems to show that formally verifying some simple properites as below in a very simple and small module takes a lot of work. Another question to consider is whether OVL could be be used with the formal tools to constrain the inputs. Seems like using OVL would make it even more difficult. And there are some things like describing the clock which don't seem possible. Code: module btrack (clk,allocate,deallocate,set); input clk;         // 1/4 cycle low active clock.  ie. high for 3, low for 1, high for 3, low for 1... input allocate;    // Allocates the data buffer.  Changes on the negedge of clk. input set;         // Makes the allocated data buffer valid.  Changes on the negedge of clk. input deallocate;  // Deallocates the data buffer.  Changes on the negedge of clk. // The inputs never occur on the same cycle and must always occur in order.  That is,  allocate, set, deallocate. reg active_r, valid_r; wire active_s, valid_s, active_in, valid_in; // psl default clock = posedge (clk); // psl property allocate_when_active = // never (allocate & active_s); // psl assert allocate_when_active; // psl property deallocate_when_not_active = // never (deallocate & ~active_s); // psl assert deallocate_when_not_active; // psl property eventually_valid_if_active = // always ( active_s -> eventually! valid_s); // psl assert eventually_valid_if_active; assign active_in = ((allocate | active_s) & ~deallocate); always @(negedge clk) begin   active_r <= active_in; end assign active_s = active_r; assign valid_in = (active_s & (set | valid_s)); always @(negedge clk) begin   valid_r <= valid_in; end assign valid_s = valid_r; endmodule Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1239 Location: Los Angeles, CA Posted: Mon May 10, 2004 3:16 pm    Post subject: Code: // psl default clock = posedge (clk); ... always @(negedge clk) begin 1. There is no reason for you not to use the same phase of the clock for your verification. You default is on posedge, Verilog vblocks are on negedge. 2. I suggest that you change the psl default clock to negedge clk. Quote: I hesitated to mention the tool name because I didn't know if I should be mentioning specific tools on this site. If you have an NDA, you cannot disclose company private information. You can mention public information (i.le., published on the vendor's site). However, this is not an IEEE group, and just like the Cooley's newsletter you can mention tools and opinions. Quote: Going through this exercise seems to show that formally verifying some simple properites as below in a very simple and small module takes a lot of work. That was not my experience with Cadence and @HDL tools. After a few interactions / questions with the vendor I found the tool and interpretation of the results very easy. By all means, fix your phasing of the clocks: ONE phase for design and verification!!! For simulation you may want to tell the tool to check at the opposite clock phase of the design (like you did). But this is only to get away from delta times and to visualize the results. This is not a necessity though! Ben 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 romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Mon May 10, 2004 3:24 pm    Post subject: Quote: By all means, fix your phasing of the clocks: ONE phase for design and verification!!! For simulation you may want to tell the tool to check at the opposite clock phase of the design (like you did). But this is only to get away from delta times and to visualize the results. This is not a necessity though! I really don't want to change my psl (and I shouldn't have to) between formal and simulation. Since the simulation tools seem to treat properties as registers, if the edges are the same, the assertion fails 1 cycle after the logic problem. This is a huge headache since often times the state of the machine is dumped at the time of the failure. So, to make the property fail on the same cycle, I use the next available edge. In this case my registers clock on the negative edge so the assertions clock on the positive edge. Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Mon May 10, 2004 3:36 pm    Post subject: Quote: That was not my experience with Cadence and @HDL tools. After a few interactions / questions with the vendor I found the tool and interpretation of the results very easy. Maybe it's just the tool I'm using that's making this difficult. However, I now have at least 10 PSL properites in an "assumptions" vunit to constrain this simple 4-input module and verify these 3 properites (and it still doesn't work). Doing this to a module where there are more than 3 unique interfaces and that internally is a lot more complex, seems like it would be quite a task. Also, I've "over constrained" the module a couple times accidentally and it passed the formal check. This seems very dangerous and hard to catch. I just couldn't believe what I had was working. So, I looked more closely and found my "over constraining" problem. Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1239 Location: Los Angeles, CA Posted: Mon May 10, 2004 3:53 pm    Post subject: Quote: I really don't want to change my psl (and I shouldn't have to) between formal and simulation. Since the simulation tools seem to treat properties as registers, if the edges are the same, the assertion fails 1 cycle after the logic problem. This is a huge headache since often times the state of the machine is dumped at the time of the failure. So, to make the property fail on the same cycle, I use the next available edge. In this case my registers clock on the negative edge so the assertions clock on the positive edge. From my observations, in simulation if your design is @ (posedge clk) and your assertions are either @ (posedge clk) or @ (negedge clk) you get the same results. By verifying your assertions at mid-bit, you basically allow 1/2 period for settling time, whereas by verifying the assertion using the same clock edge, you allow a full period. For example, if your Verilog always block clocks @ posedge clk, at that edge (assuming you're correctly using nonblocking assignments), your signals are not changing till later (similar to delta time). By having the assertions clocked at the same edge as your designs, the properties are checked just before they change. Thus, I fail to understand your argument about "the assertion fails 1 cycle after the logic problem". As for formal verification, I never tried having the assertions at a different phase thatn the design. I believe that formal verification is cycle-based anyway, and mid-cloking for assertions is meaningless. Since it is trivial to make this ONE line change in the "default clock = " statement, can you try to make that one change to make the assertion clock and the design clock at the same edge? I would like to know if that makes a difference. Another question: Is you issue the way Cadence displays the counterexamples? I understand that the display has a phase shift that will be corrected // it's really an issue on how the display is presented. 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 romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Mon May 10, 2004 4:36 pm    Post subject: I'll try some things and get back tomorrow. But I think in NCSIM (LDV5.1) when the assertion fails on a negedge, all the registers that are on a negedge get update to their new value before the simlation stops. So, when the values are dumped, the updated values are seen. Also, I think the waveform will display the updated values if you click on the transition of the assertion failure. The suggestion to use a different edge than what most registers in my design clock on came from Cadence. Seems like they do the same thing and have suggested it to others. Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1239 Location: Los Angeles, CA Posted: Mon May 10, 2004 4:41 pm    Post subject: You are mostl likely correct about what you are saying. They also suggested the same thing to me, and I used that approach in our book in some cases. Since I was not doing any dump, it made no difference to me. However, I see your point. Formal verification is different though! I would like to know your results. 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 bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Tue May 11, 2004 5:46 am    Post subject: Hi, My comments are out of sequence, but Romi wrote Quote: I've "over constrained" the module a couple times accidentally and it passed the formal check. This seems very dangerous and hard to catch Does your model checker have vacuity checking? I thought over constraining would be highlighted by vacuity of one or more of the required properties? It's hard to comment on the number of properties required without knowing something about the design, but I don't think it's fair to relate properties to pin count - the real issue I think is the number of internal states. Consider an Ethernet interface - it has one serial input but a heck of a lot of states! Finally on the subject of clocks, I think it's worth pointing out that Sugar (IBM's original name for PSL) comes from "syntactic sugaring" and under the skin PSL is really very simple and is defined by a set of re-write rules that allow multiple clocks to be flattened to un-clocked formulas, therefore no notion of clocks is strictly required within properties. You can perform the multi-clock to single clock flattening by hand (it's similar to the way I took clocks into the boolean expressions yesterday), so there ought to be no limitations on support for multi-clock systems, however: 1) I think most current model checkers require the Verilog model to be RTL, and probably struggle to support anything except one clock domain synchronous logic. 2) flattening is going to increase the number of states, thereby making the state-space problems worse. Regards Bernard Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Tue May 11, 2004 7:26 am    Post subject: staitccheck does do vacuity checks. However, from the description and examples in the manual, it doesn't seem like it would prevent over constraining. It looks like it checks for things like: always (signal == 1); always (signal == 0); My problem was that I was writing properties that, in the end, basically made the inputs never do anything. So, the internal checks never failed. Quote: It's hard to comment on the number of properties required without knowing something about the design, but I don't think it's fair to relate properties to pin count - the real issue I think is the number of internal states. Consider an Ethernet interface - it has one serial input but a heck of a lot of states! I agree with your point that the number of inputs doesn't necessarily relate to the difficulty of writing assumptions for the module. I still think it's fair to say the my example is rather simple and a more complex module would probably increase the size of the task considerably. Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Tue May 11, 2004 7:50 am    Post subject: Below is the code I ran on my previous example above. I'm now using negedge everywhere. I ran into a few problems... The first counter example shows that deallocate goes to 1 before allocate or set. This triggered the deallocate_when_not_active assertion. How can I say that allocate needs to be the first input to go to 1? A second counter example, which I don't quite understand, shows allocate going to 1 and setting the active register on the first negedge. Then, on the next negedge allocate AND deallocate go to 1 causing the allocate_when_active assertion to fire. It doesn't seem to be following a couple properties. Since set never goes to 1 before deallocate, the allocate_to_set property seems violated and also since allocate AND deallocate go to 1 on the same cycle, the same_time property seems to be violated. I wish I could insert an image here w/o having to store it to a http location. I can probably take the second counter example problem up with the vendor if the results seem suspicious. The first problem however seems like it would be a common "How do I..." problem encounter by many. Thanks. Code: clock sequence clk_seq = {clk[*3];~clk}; default clock = (negedge clk); property allocate_to_set =   always ({allocate} |=> {(~allocate & ~deallocate)[*];set}!); property set_to_deallocate =   always ({set} |=> {(~set & ~allocate)[*];deallocate}!); property deallocate_to_allocate =   always ({deallocate} |=> {(~deallocate & ~set)[*];allocate}); property same_time =   never ((allocate & set) |          (allocate & deallocate) |          (set & deallocate));           Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Tue May 11, 2004 8:38 am    Post subject: The way I was looking at vacuity checks was in the context of a property like: always { SequenceA } |=> { SequenceB }; In these circumstances, if you tighten the constraints so much that SequenceA never happens, you have vacuous satisfaction of the property. And of course if SequenceA does happen the property must be satisfied anyway, therefore vacuity is a good check constraints. I don't think it has much value in the case of a property like: always { boolean } ; however! In the specific example, I'm not sure I understand the requirement. Must set, allocate and deallocate be active for one, and only one cycle, or can they be many cycles in duration? My guess is we painted too general a picture when we were talking about the three properties. If they should be active for just one cycle I think you need properties of the form: always { a } |=> {(!a && !b && !c)[*] ; (!a && b && !c) } ! This says that once 'allocate' is true, there can be any number of cycles where there is no set, allocate or deallocate, until there is eventually a cycle where set is true but not allocate or deallocate are not. Is this the correct interpretation? If so, you'll need to change the other two properties in a similar way. I also wonder if the under this scenario the 'never' property is required? Once the allocate, set, deallocate cycle starts I don't think there is any way you can get two signals active at the same time, though I haven't had enough coffee yet to figure out what happens at the beginning! Do you have a reset signal? Perhaps that's the key to getting operations to start correctly? Regards Bernard Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Tue May 11, 2004 9:13 am    Post subject: Your example makes a lot of sense. I changed my code to use the form you mentioned and I commented out the same_time property. However, I get the exact same counter examples! The first one is obviously still there because it still hasn't be addressed. Nothing is preventing b or c (set or deallocate in my example) from going to 1 before a (allocate). The second one where the sequence goes a on the first negedge and a AND c on the next negedge is still a mystery. 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, 3, 4  Next Page 2 of 4   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.799 Seconds