1CTL(5)            CTL file format of ASIM/LIP6/CAO-VLSI lab.            CTL(5)
2
3
4

NAME

6       ctl - Control Temporal Logic file format.
7
8

DESCRIPTION

10       This  document  describes the CTL file format used by moka(1) for model
11       checking of finite states machine description.
12
13       This CTL file format subset is defined to enable classical CTL formulae
14       description.
15       A  CTL  file  is  made  of two parts: a declaration part and a formulae
16       statement part.
17
18       The declaration part described types, constants, macros and  all  vari‐
19       ables  used  in  CTL formulae.  It also describes assumption conditions
20       and initial conditions that have to be applied by  moka(1)  during  the
21       model checking.
22
23       The formulae statement part described all the CTL formulae that have to
24       be verified.
25
26       All boolean and relational VHDL operators are  supported  (see  vbe(5))
27       and also the 8 CTL operators AF, AG, AX, AU, EF, EG, EX and EU. The CTL
28       file format support also the imply boolean operator '->' and the equiv‐
29       alence operator '<=>'.
30
31

EXAMPLE

33       --  user type definition
34
35          TYPE A_ETAT_TYPE IS (A_E0, A_E1);
36          TYPE B_ETAT_TYPE IS (B_E0, B_E1);
37
38       --  variables definition
39
40          VARIABLE A_NS, A_CS : A_ETAT_TYPE;
41          VARIABLE B_NS, B_CS : B_ETAT_TYPE;
42
43          VARIABLE    ck       : BIT;
44          VARIABLE    data_in  : BIT;
45          VARIABLE    data_out : BIT;
46          VARIABLE    reset    : BIT;
47          VARIABLE    ack      : BIT;
48          VARIABLE    req      : BIT;
49
50       -- example of a macros definition
51
52          DEFINE      def1     : BOOLEAN := ack='1';
53
54       -- the assigned value can be a constant
55
56          DEFINE      c1       : BIT  := '1';
57
58       -- the assumption condition
59
60          ASSUME   ass1  := (reset='0');
61
62       -- the initial reset condition
63       -- be careful, the assumption condition is not applied
64       -- to the initial conditions.
65
66          RESET_COND init1 := (reset='1');
67
68       -- It is also possible to describe the first state
69       -- with the INITIAL keywork, as follows:
70       --
71       -- INITIAL init1 := ((A_CS=A_E0) AND (B_CS=B_E0));
72       --
73
74       -- formulae description statement part
75
76       begin
77
78          prop1 : EX( ack='1' );
79          prop2 : AG( req -> AF( ack ) );
80          prop4 : AU( req='1', ack='1');
81
82       end;
83
84

SEE ALSO

86       moka(1)
87
88
89
90
91
92ASIM/LIP6                       August 5, 2002                          CTL(5)
Impressum