Emil,
VIS makes use of the ZDD functions in CUDD for some tasks. In
particular, the synthesize_network znd restruct_fsm commands rely
extensively on ZDDs.
However, VIS does not use ZDDs instead of BDDs for the more
traditional tasks of model checking. Experiments we ran several years
ago were not encouraging.
Fabio
>>>>> "E" == Emil <Emil.Dumitrescu@imag.fr> writes:
E> Hello,
E> I recently consulted the resease documentation of CUDD, available at
E> http://vlsi.Colorado.EDU/~fabio/CUDD/cuddIntro.html
E> I can see that the CUDD package offers some support for ZDD manipulation.
E> I'd like to know whether VIS can handle ZDDs. For instance, is it possible
E> to chose between BDDs or ZDDs for representing a state space (maybe when
E> calling build_partition_mdd), and to perform the most common checks
E> (invariant or equivalence checking, model checking) ?
E> Best regards,
E> Emil
This archive was generated by hypermail 2b30 : Tue Mar 19 2002 - 22:16:27 MST