FANCY 1.1 is now available by anonymous ftp on

                        ftp.loria.fr
in directory            /pub/loria/eureca/FANCY

as compiled version or as source code.

FANCY is a BDD-based tool for formal hardware verification.
It's a collection of new and known FSM equivalence and inclusion check
algorithms with a graphical user interface.
The finite state machines (FSMs) can be of Mealy type or Moore type
and must be given in the format of the ISCAS'89 benchmark or in the blif
format (Berkeley Logic Interchange Format).
Such a collection is useful because no equivalence/inclusion
checking algorithm works well for all examples. Every one has its favorite
examples and its bad examples.

FANCY runs under Unix with the X window system (X11)
and the Tcl/Tk interpreter `wish' (version Tcl/7.3, Tk/3.6, available
by anonymous ftp on harbor.ecn.purdue.edu) for the graphical user interface.

There are compiled versions of FANCY for SUN 4, HP 9000,
DEC 5000 (due Laurence Pierre), and a Linux version for PC 486 (for the
moment only version 1.0).

New features in version 1.1:
        - equal machines are immediately recognized, i.e. machines
          with equal transition function, equal output function, and
          equal initial state, e.g. the ISCAS'89 benchmark circuit pairs
          are all equal machines
        - new option for representability algorithm: breadth first or
          depth first search strategy (before: only depth first possible)
        - new choice for representability algorithm: implicit partition
          storage with q's FIRST representability test; the representability
          test of version 1 is now called implicit with q's last
        - fsm1 files are shorter; version 1.0 fsm1 files are compatible
        - better error messages during the transformation from the
          ISCAS'89 or blif format into the internal fsm1 format, e.g.:
                "iscas format error: input variable already defined!!!"
        - original state variable names in the control_out file
        - no dynamic variable reordering during the transformation;
          this permits the user to control the variable ordering
          which he states in his ISCAS'89/blif file
        - representability algorithm optimized: transition function
          and state sets (\lambda_{i,w}) are reduced with the
          Coudert et al. cofactoring method
          (Grenoble '89/LNCS 407, and CAV'90/LNCS 531)
        - wallclock time showed before and after verification
          ("starttime, endtime"), note: the wallclock time difference
          is usually greater than the indicated runtime
        - "stop verification" button kills all running verification processes

Stefan Krischer

===============================================================================
E-mail          krischer@ti.uni-trier.de
Address         Dr. Stefan Krischer
                Universitaet Trier
                Fachbereich IV - Informatik
                D-54286 Trier
                Germany
Tel.            (+49) 651-201 2832 (office)
Fax             (+49) 651-201 3954
===============================================================================