Checkblif(1)

NAME
checkblif - blif file processor checking FSM outputs - Version v1_3

SYNTAX
checkblif [options] [options]file[.blif]

DESCRIPTION
The checkblif processor works on Finite State Machines (FSMs) described implicitly in the textual file format blif (Berkeley Logical Interchange Format), dedicated to the description of boolean circuits with latches. It tests if some user selected outputs from the FSM can be emitted in the set of the FSM possible behaviors. For each output found emitted, a minimal trace starting from an initial state leading to a state where the output is emitted is extracted. This trace is then saved in a file in the csimul format and can be played back in the graphical Esterel simulator Xes (http://www.inria.fr/meije/esterel).

The blif file name describing the FSM is given through the command line argument. Another blif file may be given with a specific option (see below). It should be a file defining a set of relations between the input signals of the FSM. It is given as a combinational circuit whose output are the valid inputs of the FSM. Typically, this file may be generated by the Esterel language compiler when relations are specified at the program source level. The list of output signals to check for emission is also given through the command line with an option specified below.

OPTIONS

-output [{] o_name [}] | { o_name1 ... o_nameN }
    The list of output signal names to check follows this option. The list is delimited with curly braces. A space character at least must separate the delimiters from the signal names. When the list has just one element, delimiters can be omitted.

-rel relation_file[.blif]
    Specify the name of a blif file defining input relations to take into account when building the FSM.

The following options can be added to the preceding ones:

-v  Verbose mode. Tell what it is doing (Default is quiet).

-help
    Display a brief description of the command line arguments on standard output. All other options are ignored.

All the described options can appear in any order. Warnings appear when incompatible or unknown options are specified.

DEFAULT
The command, without option just parses the given blif file and build the underlying FSM.

DIAGNOSTICS
The command returns with exit code 0 if (and only if) no error was detected during the treatments.

Various error or warning messages indicate parsing errors, or error related to file handling.

BUGS
Should be sent to Amar.Bouali@sophia.inria.fr.

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, INRIA(Amar.Bouali@sophia.inria.fr)
Copyright INRIA 1997.
$Revision: 1.2 $
$Date: 1997/12/10 13:34:05 $