Thursday, November 20, 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 > Digital IC > Formal verification

Subject: Conformal
Posting to forums is available to community members only.
Login or Register
Rate this topic:
   
Author Messages
anssprasad
Posts: 19
Online: User is Offline
3/13/2007 11:07 PM   
I have run into an issue: there is an 8-bit
input bus.  The 4 MSBs and the 4 LSBs are related: the LSBs are simply the
inversion of the MSBs.  So selΕ] = ~selΑ], selΔ] = ~selΐ], etc.

The original code used all 8 bits of sel (for reasons that I can only
guess).  There isn't any reason to do this in the behavioral code, and in
fact it makes the code a lot less readable.  The problem is that sel is an
input port, so LEC won't pass unless either:
  1. I use sel the way it was used in the original code
  2. I can tell Conformal the relationship between selΕ:4] and
selΑ:0].

Do anyone know a way to achieve the second option?  I'd guess that conformal
supports this, but I have no idea how.

Thanks,
Prasad
anssprasad
Posts: 19
Online: User is Offline
3/14/2007 4:54 AM  
I see that there is some formatting problem, so I am reposting with numerics replaced by english words:

I have run into an issue: there is an 8-bit
input bus.  The 4 MSBs and the 4 LSBs are related: the LSBs are simply the
inversion of the MSBs.  So sel[seven] = ~sel[three], sel[six] = ~sel[two], etc.

The original code used all 8 bits of sel (for reasons that I can only
guess).  There isn't any reason to do this in the behavioral code, and in
fact it makes the code a lot less readable.  The problem is that sel is an
input port, so LEC won't pass unless either:
  1. I use sel the way it was used in the original code
  2. I can tell Conformal the relationship between sel[seven:four] and
sel[three:zero].

Do anyone know a way to achieve the second option?  I'd guess that conformal
supports this, but I have no idea how.

Thanks,
Prasad
croy
Posts: 54
Online: User is Offline
3/14/2007 7:06 AM  
Hi Prasad

Here's one way to handle it in Conformal:

add pin constraint one_hot selΕ] selΑ] -golden
add pin constraint one_hot selΔ] selΐ] -golden
add pin constraint one_hot selΓ] selΏ] -golden
add pin constraint one_hot selΒ] selΎ] -golden

With these set then logic like this would pass:

golden
assign out1 = selΕ]&selΑ] | selΔ]&selΐ] | selΓ]&selΏ] | selΒ]&selΎ]

revised
assign out1 = 1'b0;

Chrystian
bryan
Posts: 25
Online: User is Offline
3/14/2007 1:56 PM  
Chystian,

There isn't a way to state inverted equivalence? Seems that would be more appropriate and provide more positive checking.
Regards,
Bryan
croy
Posts: 54
Online: User is Offline
3/14/2007 2:05 PM  
Hi Bryan

Yep, there is. That's why I said 'here's *one* way' :-)

Here's another:

add pin equi selΕ] -invert selΑ] -golden
add pin equi selΔ] -invert selΐ] -golden
add pin equi selΓ] -invert selΏ] -golden
add pin equi selΒ] -invert selΎ] -golden

The end result is the same but you're right that this is more explicit than 'one_hot'.

Chrystian
anssprasad
Posts: 19
Online: User is Offline
3/15/2007 10:37 PM  
Thanks Chrystian,

It was of great help.

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


ActiveForums 3.6
     
Copyright 2006 Cadence Design Systems, Inc.