From: Fabio Somenzi (Fabio_at_colorado.edu)
Date: Tue Jun 22 2004 - 15:55:39 MDT
Use `==' instead of `=' to compare two signals for equality.
Fabio
>>>>> "F" == Fabio <fabio.marcone_at_libero.it> writes:
F> Hi!
F> I've some problems to describe a condition to verify in vis
F> (bounded_model_checking).
F> I've 2 models:
F> A with output a0...an
F> B with output b0...bn
F> I need to verify that a0=b0 and ...and an=bn and I wrote in the ltl file:
F> G((A.a0=B.b0)*...*(A.an=B.bn));
F> but vis error message indicates that A.a0 isn't a known node. why?
F> So I wrote
F> G((a0=b0)*...*(an=bn));
F> but in this way there is an error in the RHS.
F> Can we help me?
F> Thanks,
F> Fabio Marcone
This archive was generated by hypermail 2.1.7 : Tue Jun 22 2004 - 15:56:19 MDT