bmc and "formula undecided"

From: Fabio (fabio.marcone_at_libero.it)
Date: Sun Jul 04 2004 - 10:35:09 MDT

Hi!

I've some problems with bounded_model_check in vis.

For example, I've this blif:

.model main

.inputs in1 in2

.outputs out1 out2

.subckt and a0=in1 a1=in2 out=out1

.subckt and a0=in2 a1=in1 out=out2

.end

.model and

.inputs a0 a1

.outputs out

.names a0 a1 out

0 0 0

0 1 0

1 0 0

1 1 1

.end

if I want to check that out1=out2:

G(out1==out2);

but vis message is:

Formula: G((out1=1 ^ out2=0))

# BMC: formula undecided

why? what's wrong?

Thanks in advance,

Fabio Marcone

This archive was generated by hypermail 2.1.7 : Sun Jul 04 2004 - 10:37:18 MDT