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- "How do I..." Goto page Previous  1, 2, 3, 4  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: Tue May 11, 2004 9:49 am    Post subject: Your definition of vacuous makes more sense than what I got out of the Cadence documentation (LDV5.1). It would be nice if the tool indicated that an enabling condition could not be met. Thanks for your help. Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Tue May 11, 2004 1:22 pm    Post subject: As I suggested in my first email, I think you will probably need to take some kind of reset condition into the properties, or maybe add an additional property of the form: always { fell(reset) } |=> { (!a&&!b&&!c)[*];(a&&!b&&!c); ... }; to be sure the allocate is the first to happen. I too am puzzled about the second problem and need to get my head around that, unless it's another manifestation of the same reset problem - sometimes tools don't report all, or even the simple to understand counter cases. Perhaps you could implement the reset constraint first, and let us know if any of the other problems go away? Bernard Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Tue May 11, 2004 2:11 pm    Post subject: There is no reset in my example design or in the designs I work on. All our registers are statically scanned to an initialized state. Maybe I could do something like this instead. Will this make a occur first? Code: property not_b_or_c_until_a  =   1'b1 -> (~b & ~c) until_ a; Note from the moderator: this topic has been split to this topic Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Tue May 11, 2004 5:33 pm    Post subject: Quote: Will this make 'a' occur first? The simple answer is sorry, I have no idea. Formal model checking is GREAT because it checks everything exhaustively, without the need for complex testbenches and coverage feedback. Now however we don't actually want it to check some combinations, so we're trying to constrain it into skipping those, without having the necessary signals (ie a reset). How complex is your scanning process? Can't this be described within the constraints in some way? What stops the design running until the setup is complete? Do any of the Cadence AE's have any idea how to handle this kind of initialization? Regards Bernard Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Tue May 11, 2004 6:02 pm    Post subject: Quote: How complex is your scanning process? Can't this be described within the constraints in some way? What stops the design running until the setup is complete? We run our simulations on a design without the scan strings built into the register models. We use TCL to load our registers at time 0 in simulation. During a real static scan the clocks are not on. That's what prevents the design from running. I'll be having some talks with some Cadence people in the near future. Hopefully, they can come up with a way to allow us to model our design for FV. Thanks for your comments. Back to top vhdlcohen Industry Expert Joined: Jan 05, 2004 Posts: 1238 Location: Los Angeles, CA Posted: Tue May 11, 2004 6:27 pm    Post subject: In formal verification you need to assume a reset. In our traffic light controller book example, we used the following: Code: vunit clk_rst (trafficlight) { clock sequence const_clk is { clk; not clk } ; property rst_low_first_cycle_then_high is {true} |-> { !reset_n ; reset_n}; property rst_high_after_first_cycle is always {reset_n=’1’} |=> {reset_n=’1’}; assume rst_low_first_cycle_then_high ; assume rst_high_after_first_cycle; } With scan, you can do something similar. Code:   property rst_low_first_1000cycle_then_high is {true} |-> { scan_enb and scan_data='1' ; [*1000]; not scan_enb}; property rst_high_after_first_1000cycle is always {[*1000]; not scan_enb} |=> {not scan_enb}; assume rst_low_first_1000cycle_then_high ; assume rst_high_after_first_1000cycle; } This may work.  Let us know. _________________ 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: Tue May 11, 2004 6:54 pm    Post subject: Most of our simulation is done without the scan inserted into the verilog. We just use TCL to initialize. Changing the scan ports with this design has no effect because they are not tied to anything. Our registers are just basically what I had in my example. Code: always @(negedge clk) begin    reg1_r <= reg1_in; end assign reg1_s = reg1_r; This models a master/slave register. Both the master and the slave change on the same edge, but it still works in simulation the same way a real master/slave register would. ie. you can assign the reg1_s signal to another negedge clk register w/o it being a race condition. We do this to maximize simulator performance which is critical for our verification. The bottom line is that I still don't think we have a solution to constraining how the inputs start up for FV with the verilog coding style we use. My example property attempting to not allow b or c to go to 1 until a went to 1 did not work. I can't explain why. I think I'm stuck for now. Note from the moderator: the topic of using master/slave latches and FV has been split to this topic Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Wed May 12, 2004 1:25 pm    Post subject: Having thought about this some more, I wondered what happens if your latches get written between allocate and deallocate? That is to say, is the latch writing acting like an initialization? If that is the case, isn't the simplest answer to wrap your code in a minimal initialization circuit for FV? In that way you create a reset/init signal as part of your constraints and use you init circuit to write the latches as required? That way the model checker will automatically verify the circuit receiving initialization at any stage of the alloc / set / dealloc sequence. Regards Bernard Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Wed May 12, 2004 1:42 pm    Post subject: Quote: If that is the case, isn't the simplest answer to wrap your code in a minimal initialization circuit for FV? In that way you create a reset/init signal as part of your constraints and use you init circuit to write the latches as required? That way the model checker will automatically verify the circuit receiving initialization at any stage of the alloc / set / dealloc sequence. Not sure what you mean by wrap. I don't think I should have to change the code in my btrack module at all just for the model checker. Were you thinking of another module that used OOMRs to init the registers? It doesn't seem likely that the tool would like OOMRs. So, it's probably not what you meant. I think you are telling me to put a reset in my design even though there isn't one in reality. That doesn't seem resonable. Quote: Having thought about this some more, I wondered what happens if your latches get written between allocate and deallocate? I'm lost here. The only thing that can update the latches between allocate and deallocate is set and set can only update the valid_r latch. The scan logic is not in this level of modelling if you were refering to the scan logic writing the latch. Code: 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; Back to top bdeadman Senior Joined: Jan 06, 2004 Posts: 204 Location: Austin, TX Posted: Wed May 12, 2004 1:52 pm    Post subject: Quote: Not sure what you mean by wrap No, it's vital that you absolutely do not modify your module at all. I was suggesting you create a small module used for FV purposes only that instantiates your module un-modified, but formally verify at the level of the new module - the new module would be a skinny layer (wrapper) around your module to provide initialization equivalent to the scan registers. Quote: if you were refering to the scan logic writing the latch Yes, exactly that - what happens if the scan register writes in the middle of an operation? Isn't that part of what you want to verify, to make sure, for example, that the module doesn't do something stupid like lock up? Regards Bernard Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Wed May 12, 2004 1:59 pm    Post subject: Quote: No, it's vital that you absolutely do not modify your module at all. I was suggesting you create a small module used for FV purposes only that instantiates your module un-modified, but formally verify at the level of the new module - the new module would be a skinny layer (wrapper) around your module to provide initialization equivalent to the scan registers. I see. A reset for the input lines to bring them up in a good state. That's a great idea. I'll try it. Quote: Yes, exactly that - what happens if the scan register writes in the middle of an operation? Isn't that part of what you want to verify, to make sure, for example, that the module doesn't do something stupid like lock up? If my code had scan logic in, then I agree that we would also want to verify that. At another level of modelling our code does have the scan logic inserted so this will be important. In the beginning we don't insert it. Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Wed May 12, 2004 3:34 pm    Post subject: I'm seeing different results with wrapping my original module in the module below. However, I still see multiple allocates before set. Two different vendors' tools are giving the same results (that's a good thing, I guess). Code: module btrack_tb(allocate, set, deallocate, reset, clk,                  allocate_out, set_out, deallocate_out); input clk; input allocate,set,deallocate,reset; output allocate_out,set_out,deallocate_out; reg allocate_out,set_out,deallocate_out; always @(negedge clk) begin   if(~reset)begin     allocate_out <= allocate;     set_out <= set;     deallocate_out <= deallocate;   end else begin     allocate_out <= 0;     set_out <= 0;     deallocate_out <= 0;   end end btrack btrack0(   .clk(clk),   .allocate(allocate_out),   .set(set_out),   .deallocate(deallocate_out)); endmodule Code: default clock = (negedge clk); property reset_high_to_start =   {1'b1} |-> {reset;~reset}; property reset_low_after_start =   always ({~reset} |=> {~reset}); property allocate_to_set =   always ({allocate} |=> {(~allocate & ~set & ~deallocate)[*];           ~allocate & set & ~deallocate}!); property set_to_deallocate =   always ({set} |=> {(~set & ~deallocate & ~allocate)[*];            ~allocate & ~set & deallocate}!); property deallocate_to_allocate =   always ({deallocate} |=> {(~deallocate & ~allocate & ~set)[*];           allocate & ~set & ~deallocate}); property same_time =   never ((allocate & set) |          (allocate & deallocate) |          (set & deallocate)); Back to top confused Senior Joined: Jan 09, 2004 Posts: 185 Posted: Thu May 13, 2004 3:35 am    Post subject: There has to be a general method to provide the initial state. This method should be shared by both simulation and formal verification if possible. (1) Using Tcl (or C/C++/perl or a tool-specific language) to set initial values is a popular method for simulation. (2) Simulating the real hardware operations of the initialization sequence (scan or writing software-addressable registers after reset) is another. The second method can add too much complexity for formal verification. At least, the properties may or may not be applicable to both the initialization sequence and the sequence afterward. 0-In uses simulation to get the initial state before starting formal verification to reduce the formal verification complexity. The first method may not add as much complexity, but it may not be portable among the tools (at least for now). Verilog initial blocks can be used for this method in most cases, and it can be more portable. However, it may not be portable either if non-synthesizable constructs are used in these initial blocks. Formal verification tools may not take any initial blocks at all simply because synthesis tools do not traditionally need initial blocks. Is there anything like initial blocks in VHDL? Is there a third method? Back to top Janick Site Admin Joined: Nov 29, 2003 Posts: 1382 Location: Ottawa, ON Canada Posted: Thu May 13, 2004 6:25 am    Post subject: confused wrote: Is there a third method? Maybe revisit the decision not to have a reset? romi never provided details on his application and there may be some very good reasons for not having a reset. But could those reasons have become less important in the face of increasing verification complexities? Back to top romi Senior Joined: Feb 28, 2004 Posts: 88 Location: Minnesota Posted: Thu May 13, 2004 6:36 am    Post subject: Quote: romi never provided details on his application and there may be some very good reasons for not having a reset. But could those reasons have become less important in the face of increasing verification complexities? I think I mentioned somewhere that we statically scan our initial state in instead of using a reset to initialize. None of the designs I've worked on use a reset, so I don't know much about designs that use reset, but it sure seems like being able to not hardcode a reset value sure has many advantages. It allows us to programmatically change the operations of our ASIC by just changing the initialized state. If this was hardcoded, this doesn't seem possible. I guess I don't understand why the reasons for not having a reset would become less important as verification becomes more complex. It seems just the opposite to me based on my assessment of why we don't use a reset. As verification becomes more complex, a design would want much more programability to workaround problems and to tune the design to maximize performance. 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 3 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.256 Seconds