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: IFV, prove one assertion
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
weberrm
Posts: 0
Online: User is Offline
11/13/2007 7:57 AM  
Sometimes I want to prove just one assertion or cover.  I run the steps below filling in the last assertion step with the assertion or cover requested.
 
assertion -delete -cover
assertion -delete -specification
assertion -add assertion [-specification | -cover]
prove
 
Any suggestions on how to automate this?  Ideally, I would like to right-click the assertion and click prove from menu.

Thanks!
stephenh
Posts: 77
Online: User is Offline
11/13/2007 8:06 AM  
I would write a TCL procedure that takes the assertion name as the parameter ( or the type as you asked for):

proc only_prove { prop_name } {
assertion -delete -cover
assertion -delete -specification
assertion -add $prop_name
prove
}

then you can just do:
only_prove tb.prop1
etc

You can also use this idea to make a new GUI toolbar button.
Take a look at the following article to see how it's done:
http://www.cdnusers.org/Forums/tabid/52/forumid/64/postid/3933/view/topic/Default.aspx
Steve H.
jb
Posts: 16
Online: User is Offline
11/13/2007 9:16 AM  
Steve,

I implemented the button as you suggested. This works well in conjunction with a custom button that runs the following tcl code for this button:

only_prove %s

Make sure you click the box for "selection sensitive to selection" and select from the drop down to make this a FormalVerifier script command.

Consider not delelting all assertions in the proc as you will not be able to get results at the end of the run via the assertion -show command. In otherwords, put the commands:

ass -del -all

in the base tcl script and have the proc add the specified assertion and prove. You will then accumulate results in the gui and ass -show tcl command.

JB
Posting to forums is available to community members only.
Login or Register


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.