From: Fabio (fabio.marcone_at_libero.it)
Date: Tue Jun 22 2004 - 15:49:57 MDT
I forgot that models are defined in blif (not in blifmv).
Fabio
----- Original Message -----
From: "Fabio" <fabio.marcone_at_libero.it>
To: <vis-users_at_lists.colorado.edu>
Sent: Tuesday, June 22, 2004 11:45 PM
Subject: ltl formula
> Hi!
> I've some problems to describe a condition to verify in vis
> (bounded_model_checking).
> I've 2 models:
> A with output a0...an
> B with output b0...bn
>
> I need to verify that a0=b0 and ...and an=bn and I wrote in the ltl file:
> G((A.a0=B.b0)*...*(A.an=B.bn));
>
> but vis error message indicates that A.a0 isn't a known node. why?
> So I wrote
> G((a0=b0)*...*(an=bn));
>
> but in this way there is an error in the RHS.
>
> Can we help me?
>
> Thanks,
> Fabio Marcone
>
>
This archive was generated by hypermail 2.1.7 : Tue Jun 22 2004 - 15:50:13 MDT