Provided by: alliance_5.0-20110203-4_i386 bug

NAME

       ctl - Control Temporal Logic file format.

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)