Xeve(1)

NAME
xeve - An Esterel Verification Environment - Version v1_3

SYNTAX
xeve [options] [wish_options] [file[.blif]]

DESCRIPTION
Xeve is a graphical interface environment for the (symbolic) analysis and verification of Esterel programs modeled as Finite State Machines (FSM). Its main features are:

    FSM model construction

    FSM minimization and visualization

    Output emission status checking used as a back-end of model-checking of safety properties expressed by observers.

Minimized FSMs can be graphically explored within the tool Atg (http://www.inria.fr/meije/verification). Diagnostic paths generated from model-checking are loadable in the tape reader of the Esterel graphical simulator Xes (http://www.inria.fr/meije/esterel). Xeve GUI is implemented in Tcl/Tk. FSMs are represented symbolically with BDDs using the TiGeR system data structures and libraries. It is an integration of two unix processors called bliffc2 and checkblif. Xeve command can be sent either with a blif file name argument or without. In both case the graphical panel of the interface is displayed and in the first case, the given file is loaded in the panel.

OPTIONS

Options "wish_options" are those accepted by the wish(1) program, but the "-help" option, trapped by xeve. The following options are accepted by xeve:

-rel relation_file
    Specifies a relation blif file.

-help
    Gives a help on the xeve command syntax.

-info
    Gives informations on the xeve program (version number, date, author,...).

The two preceding options exit the program without doing anything else.

SEE ALSO
Our WWW site, pages: http://www.inria.fr/meije/verification/esterel
http://www.inria.fr/meije/verification
http://www.inria.fr/meije/esterel

IDENTIFICATION
Author: Amar Bouali (Amar.Bouali@sophia.inria.fr)
Copyright INRIA Sophia Antipolis, 1997 $Revision: 1.4 $
$Date: 1997/12/10 13:34:05 $