From: Fabio Somenzi (Fabio_at_colorado.edu)
Date: Mon Jul 05 2004 - 15:35:10 MDT
The bmc command takes as option (-k) the maximum length of the
counterexample. If there is no counterexample up to that length, then
the formula is undecided.Traditional BMC, which is what is implemented
in VIS 2.0, is not a complete method.
The default for the -k option is 1. One normally specifies the value
explicitly.
Fabio
>>>>> "F" == Fabio <fabio.marcone_at_libero.it> writes:
F> Hi!
F> I've some problems with bounded_model_check in vis.
F> For example, I've this blif:
F> .model main
F> .inputs in1 in2
F> .outputs out1 out2
F> .subckt and a0=in1 a1=in2 out=out1
F> .subckt and a0=in2 a1=in1 out=out2
F> .end
F> .model and
F> .inputs a0 a1
F> .outputs out
F> .names a0 a1 out
F> 0 0 0
F> 0 1 0
F> 1 0 0
F> 1 1 1
F> .end
F> if I want to check that out1=out2:
F> G(out1==out2);
F> but vis message is:
F> Formula: G((out1=1 ^ out2=0))
F> # BMC: formula undecided
F> why? what's wrong?
F> Thanks in advance,
F> Fabio Marcone
This archive was generated by hypermail 2.1.7 : Mon Jul 05 2004 - 15:35:57 MDT