Re: ZBDD support

From: Emil (Emil.Dumitrescu@imag.fr)
Date: Wed Mar 20 2002 - 02:06:40 MST

  • Next message: Fabio Somenzi: "Re: ZBDD support"

    Dear Fabio,

    Thank you for your answer.

    > 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.

    Does this mean that zdd manipulations are not at all fit for symbolic FSM
    traversal ?
    Is there a particular zdd operation which introduces a significant
    computation/memory overhead ?

    Thank you in advance.

    Emil

    > 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
    >



    This archive was generated by hypermail 2b30 : Wed Mar 20 2002 - 02:20:47 MST