1MOKA(1) CAO-VLSI Reference Manual MOKA(1)
2
6 MOKA - Model checker ancestor
7
10 This software belongs to the ALLIANCE CAD SYSTEM developed by the ASIM
11 team at LIP6 laboratory of Université Pierre et Marie CURIE, in Paris,
12 France.
13 Web : http://asim.lip6.fr/recherche/alliance/
15 E-mail : alliance-users@asim.lip6.fr
16
18 moka [-VDB] fsm_filename ctl_filename
19
21 moka is a CTL model checker.
22 Made to run on FSM or RTL descriptions, moka supports the same VHDL
24 subset as syf or boom (for further informations about this subset see
25 SYF(1), BOOM(1), FSM(5), VBE(5) ). Nevertheless moka imposes that each
26 register of the behavioral description have the same clock condition
27 and that there are no tristate or multiplexed buses. In particular
28 VHDL type MUX_BIT and WOR_BIT aren't not supported.
29 First of all moka build the fonction transition of the FSM using a
30 Reduced Ordered Binary Decision Diagrams representation.
31 It then applies the initial conditions to find the first state (keyword
32 INITIAL and/or RESET_COND in the CTL(5) file format).
33 After it computes a symbolic simulation of the FSM in order to find all
34 reachable states. This computation takes into account the assumptions
35 conditions (ASSUME keyword in the CTL(5) file format).
36 moka finally verifies one by one each CTL formulae. (see CTL(5) for
37 CTL file format details).
38
41 For each CTL sub-expression moka will return the set of states that
42 verifies the formula. For example EX(p) will return the set of reach‐
43 able states that verifies EX(p).
44 CTL operators :
45 EX(p) : returns all states which have almost one primary state
46 successor that verifies p.
47 EU(p,q) : returns all states that are the root of almost one
48 path, such that p is true until q is always true.
49 EG(p) : returns all states that are the root of almost one path,
50 such that p is always true.
51 AX(p) : returns all states which have all their primary state
52 successor that verifies p.
53 AU(p,q) : returns all states that are the root of only pathes
54 from which p is true until q is always true.
55 AG(p) : returns all states that are the root of only pathes,
56 such that p is always true.
57
62 MBK_WORK_LIB gives the path for the description and the CTL file. The
64 default value is the current directory.
65 MBK_CATA_LIB gives some auxiliary pathes for the descriptions and the
68 CTL file. The default value is the current directory.
69
71 -V Sets verbose mode on. Each step of the model checking is displayed
72 on the standard output.
73 -D Sets debug mode on. Each step of the model checking is detailed on
75 the standard output. In particular all states set are displayed for
76 each CTL sub-expression.
77 -B The input file is a VHDL description using the Alliance VHDL subset
79 (see VBE(5) file format).
80
82 -- A multi fsm example
83 ENTITY example is
85 PORT
86 (
87 ck : in BIT;
88 data_in : in BIT;
89 reset : in BIT;
90 data_out : out BIT
91 );
92 END example;
93 ARCHITECTURE FSM OF example is
96 TYPE A_ETAT_TYPE IS (A_E0, A_E1);
98 SIGNAL A_NS, A_CS : A_ETAT_TYPE;
99 TYPE B_ETAT_TYPE IS (B_E0, B_E1);
101 SIGNAL B_NS, B_CS : B_ETAT_TYPE;
102 --PRAGMA CURRENT_STATE A_CS FSM_A
104 --PRAGMA NEXT_STATE A_NS FSM_A
105 --PRAGMA CLOCK ck FSM_A
106 --PRAGMA FIRST_STATE A_E0 FSM_A
107 --PRAGMA CURRENT_STATE B_CS FSM_B
109 --PRAGMA NEXT_STATE B_NS FSM_B
110 --PRAGMA CLOCK ck FSM_B
111 --PRAGMA FIRST_STATE B_E0 FSM_B
112 SIGNAL ACK, REQ, DATA_INT : BIT;
114 BEGIN
116 A_1 : PROCESS ( A_CS, ACK )
118 BEGIN
119 IF ( reset = '1' )
120 THEN A_NS <= A_E0;
121 DATA_OUT <= '0';
122 REQ <= '0';
123 ELSE
124 CASE A_CS is
125 WHEN A_E0 =>
126 IF ( ACK ='1') THEN A_NS <= A_E1;
127 ELSE A_NS <= A_E0;
128 END IF;
129 DATA_OUT <= '0';
130 REQ <= '1';
131 WHEN A_E1 =>
132 IF ( ACK ='1') THEN A_NS <= A_E1;
133 ELSE A_NS <= A_E0;
134 END IF;
135 DATA_OUT <= DATA_INT;
136 REQ <= '0';
137 END CASE;
138 END IF;
139 END PROCESS A_1;
140 A_2 : PROCESS( ck )
142 BEGIN
143 IF ( ck = '1' AND NOT ck'STABLE )
144 THEN A_CS <= A_NS;
145 END IF;
146 END PROCESS A_2;
147 -------
149 B_1 : PROCESS ( B_CS, ACK )
151 BEGIN
152 IF ( reset = '1' )
153 THEN B_NS <= B_E0;
154 DATA_INT <= '0';
155 ACK <= '0';
156 ELSE
157 CASE B_CS is
158 WHEN B_E0 =>
159 IF ( REQ ='1') THEN B_NS <= B_E1;
160 ELSE B_NS <= B_E0;
161 END IF;
162 DATA_INT <= '0';
163 ACK <= '0';
164 WHEN B_E1 =>
165 IF ( REQ ='1') THEN B_NS <= B_E1;
166 ELSE B_NS <= B_E0;
167 END IF;
168 DATA_INT <= DATA_IN;
169 ACK <= '1';
170 END CASE;
171 END IF;
172 END PROCESS B_1;
173 B_2 : PROCESS( ck )
175 BEGIN
176 IF ( ck = '1' AND NOT ck'STABLE )
177 THEN B_CS <= B_NS;
178 END IF;
179 END PROCESS B_2;
180 END FSM;
182
185 -- A CTL file example
186 TYPE A_ETAT_TYPE IS (A_E0, A_E1);
188 TYPE B_ETAT_TYPE IS (B_E0, B_E1);
189 VARIABLE A_NS, A_CS : A_ETAT_TYPE;
191 VARIABLE B_NS, B_CS : B_ETAT_TYPE;
192 VARIABLE ck : BIT;
194 VARIABLE data_in : BIT;
195 VARIABLE data_out : BIT;
196 VARIABLE reset : BIT;
197 VARIABLE ack : BIT;
198 VARIABLE req : BIT;
199 RESET_COND init1 := (reset='1');
201 ASSUME ass1 := (reset='0');
202 begin
204 prop1 : EX( ack='1' );
206 prop2 : AG( req -> AF( ack ) );
207 prop4 : AU( req='1', ack='1');
208 end;
210
213 moka -V example example
214
217 syf (1), fsp (1), fsm (5), ctl (5), vbe(5).
218ASIM/LIP6 August 5, 2002 MOKA(1)