Conformal

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

Hi Prasad

Here's one way to handle it in Conformal:

add pin constraint one_hot sel[7] sel[3] -golden
add pin constraint one_hot sel[6] sel[2] -golden
add pin constraint one_hot sel[5] sel[1] -golden
add pin constraint one_hot sel[4] sel[0] -golden

With these set then logic like this would pass:

golden
assign out1 = sel[7]&sel[3] | sel[6]&sel[2] | sel[5]&sel[1] | sel[4]&sel[0];

revised
assign out1 = 1'b0;

Chrystian

Chystian,

There isn't a way to state inverted equivalence? Seems that would be more appropriate and provide more positive checking.

Hi Bryan

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

Here's another:

add pin equi sel[7] -invert sel[3] -golden
add pin equi sel[6] -invert sel[2] -golden
add pin equi sel[5] -invert sel[1] -golden
add pin equi sel[4] -invert sel[0] -golden

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

Chrystian

Thanks Chrystian,

It was of great help.

Prasad.