Xeve(1) manual page

Table of Contents

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

Table of Contents

- Name
- Syntax
- Description
- Options
- See Also
- Identification

Back To Main Manual Page