CTL(5)                                              CTL file format of ASIM/LIP6/CAO-VLSI lab.                                              CTL(5)

NAME

       ctl - Control Temporal Logic file format.

ORIGIN

       This  software  belongs  to  the  ALLIANCE CAD SYSTEM developed by the ASIM team at LIP6 laboratory of Universite Pierre et Marie CURIE, in
       Paris, France.

       Web : http://asim.lip6.fr/recherche/alliance/
       E-mail : alliance-users@asim.lip6.fr

DESCRIPTION

       This document describes the CTL file format used by moka(1) for model checking of finite states machine description.

       This CTL file format subset is defined to enable classical CTL formulae description.
       A CTL file is made of two parts: a declaration part and a formulae statement part.

       The declaration part described types, constants, macros and all variables used in CTL formulae.  It also  describes  assumption  conditions
       and initial conditions that have to be applied by moka(1) during the model checking.

       The formulae statement part described all the CTL formulae that have to be verified.

       All  boolean  and  relational VHDL operators are supported (see vbe(5)) and also the 8 CTL operators AF, AG, AX, AU, EF, EG, EX and EU. The
       CTL file format support also the imply boolean operator '->' and the equivalence operator '<=>'.

EXAMPLE

       --  user type definition

          TYPE A_ETAT_TYPE IS (A_E0, A_E1);
          TYPE B_ETAT_TYPE IS (B_E0, B_E1);

       --  variables definition

          VARIABLE A_NS, A_CS : A_ETAT_TYPE;
          VARIABLE B_NS, B_CS : B_ETAT_TYPE;

          VARIABLE    ck       : BIT;
          VARIABLE    data_in  : BIT;
          VARIABLE    data_out : BIT;
          VARIABLE    reset    : BIT;
          VARIABLE    ack      : BIT;
          VARIABLE    req      : BIT;

       -- example of a macros definition

          DEFINE      def1     : BOOLEAN := ack='1';

       -- the assigned value can be a constant

          DEFINE      c1       : BIT  := '1';

       -- the assumption condition

          ASSUME   ass1  := (reset='0');

       -- the initial reset condition
       -- be careful, the assumption condition is not applied
       -- to the initial conditions.

          RESET_COND init1 := (reset='1');

       -- It is also possible to describe the first state
       -- with the INITIAL keywork, as follows:
       --
       -- INITIAL init1 := ((A_CS=A_E0) AND (B_CS=B_E0));
       --

       -- formulae description statement part

       begin

          prop1 : EX( ack='1' );
          prop2 : AG( req -> AF( ack ) );
          prop4 : AU( req='1', ack='1');

       end;

SEE ALSO

       moka(1)

BUG REPORT

       This tool is under development at the ASIM department of the LIP6 laboratory.
       We need your feedback to improve documentation and tools.

ASIM
/LIP6                                                         August 5, 2002                                                            CTL(5)