Friday, November 21, 2008     Register | Login | Search | Contact Us
     
   
     
     

Many of you already received communications about the move of the Cadence user community into cadence.com. And many of you have already joined, with over 4000 registrations in the first two weeks.

The new Cadence Community enhances the ability of Cadence users to connect and collaborate. In addition to moving the community into cadence.com -- enabling single sign-on for community, Sourcelink and Cadence events -- the new site is organized around nine technology segments, giving you easy access to product information, training, forums and blogs. Some of the new features include:
  • Ability to respond to posts via e-mail
  • Technology-specific blogs
  • Latest Web 2.0 social networking capabilities
  • Public profile options
  • Private messaging
  • Friends lists
Visit the new Cadence Community today at www.cadence.com/community and join the discussions!

Registration note: Due to the scope of the enhancements and the new SSO registration system, we were not able to migrate existing cdnusers.org member accounts. So new registrations are required, but this enables a broader set of functionality we think you'll enjoy.

Forum note: Under the guidance of forum moderators, we have taken the 20+ cdnusers.org forums and consolidated them into 11 forums on the new site. Posts have been brought over so you can leverage that posting history. CDNusers forums will be set to read only starting 7/30, and cdnusers.org will be redirected to the new community on 8/4.

Best regards,
Mike and Tom

Michael A. Catrambone - Steering Committee Chairman
Distinguished Engineer
PCB/Mechanical
UTStarcom, Inc.

Tom Diederich
Cadence Community Manager
Home
Forums
Forums > Functional Verification > Assertion-Based Verification and Formal Analysis

Subject: keeping rst asserted n clocks into the proof
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
jb
Posts: 16
Online: User is Offline
11/19/2006 12:34 PM  
Anyone know how to keep rst_n asserted 16  clocks iinto the proof and then deassert forever  with SVA?  I can do this easily in PSL by using assume and omitting always as in the following PSL:

// Assert rst_n for 16 clocks, then deassert for one clock. Note absense of "always"
// It fires once only during the clock 1
// psl assume_rst_n_low_16: assume {!rst_n[*16]rst_n} @ (posedge clk);
 
// This property ensures rst_n stays high once it goes high from previous property.
// psl assume_rst_n_high_rest_of_time: assume always {rst_n}|=> {rst_n};

I am trying avoid auxilliary code with SVA but I have not come up with a clean way to avoid the aux code.  In fact the aux code I have requires an undriven signal to code a trigger for clock 1 to implement the equivalent of PSL assume_rst_n_low_16 property above.

JB
foster
Posts: 0
Online: User is Offline
11/19/2006 9:15 PM  
I don't want to get too sophistical, but I look at SVA as just another kind of auxiliary verification logic, so I don't understand the motivation for the question. SVA as well as auxiliary logic should be encapsulated into ifdef pragmas anyway to avoid downstream problems in the flow.

The reason I am saying this is because I don't see a way to write this without aux code in SVA (until IFV supports assertions inside procedural initial blocks, which probably no formal tool supports).
jb
Posts: 16
Online: User is Offline
11/20/2006 8:47 AM  
Foster,

Thanks for confirming you see no other way than using axilliary code to implement this in SVA.  I agree that all this would be encapsulated within `ifdefs to eliminate the code from issues with downstream flow.

I was simply trying to see if there was a way to implement the functionality in SVA that was possible in PSL.  I have dealt with requests before to keep rst_n asserted into a proof with PSL up till now.  As there are more and more SVA users I wanted to have an implementation in SVA handy for these users.

jb
Posting to forums is available to community members only.
Login or Register
Forums > Functional Verification > Assertion-Based Verification and Formal Analysis > keeping rst asserted n clocks into the proof


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.