240 lines
5.4 KiB
Groff
240 lines
5.4 KiB
Groff
.\" @(#) 02/08/05 UPMC; Author: Jacomme L.
|
|
.pl -.4
|
|
.TH MOKA 1 "August 5, 2002" "ASIM/LIP6" "CAO\-VLSI Reference Manual"
|
|
.SH NAME
|
|
.TP
|
|
MOKA \- Model checker ancestor
|
|
.so man1/alc_origin.1
|
|
.SH SYNOPSIS
|
|
.TP
|
|
\f4moka [\-VDB] fsm_filename ctl_filename
|
|
.br
|
|
.SH DESCRIPTION
|
|
.br
|
|
\fBmoka\fP is a CTL model checker.
|
|
.br
|
|
|
|
Made to run on FSM or RTL descriptions, \fBmoka\fP supports the same VHDL subset
|
|
as syf or boom (for further informations about this subset see SYF(1), BOOM(1), FSM(5), VBE(5) ).
|
|
Nevertheless \fBmoka\fP imposes that each register of the behavioral description have
|
|
the same clock condition and that there are no tristate or multiplexed buses.
|
|
In particular VHDL type MUX_BIT and WOR_BIT aren't not supported.
|
|
.br
|
|
First of all \fBmoka\fP build the fonction transition of the FSM using
|
|
a Reduced Ordered Binary Decision Diagrams representation.
|
|
.br
|
|
It then applies the initial condition to find the first state (keyword INITIAL
|
|
in the CTL(5) file format).
|
|
.br
|
|
After it computes a symbolic simulation of the FSM in order
|
|
to find all reachable states. This computation takes into account the
|
|
assumptions conditions (ASSUME keyword in the CTL(5) file format).
|
|
.br
|
|
\fBmoka\fP finally verifies one by one each CTL formulae.
|
|
(see CTL(5) for CTL file format details).
|
|
|
|
.SH CTL OPERATORS
|
|
.PP
|
|
For each CTL sub-expression \fBmoka\fP will return the set of states that verifies
|
|
the formula. For example EX(p) will return the set of reachable states that verifies
|
|
EX(p).
|
|
.br
|
|
CTL operators :
|
|
.RS
|
|
.br
|
|
EX(p) : returns all states which have almost one primary state successor that
|
|
verifies \fBp\fP.
|
|
.br
|
|
EU(p,q) : returns all states that are the root of almost one path, such that \fBp\fP is true
|
|
until \fBq\fP is always true.
|
|
.br
|
|
EG(p) : returns all states that are the root of almost one path, such that \fBp\fP is always true.
|
|
.br
|
|
AX(p) : returns all states which have all their primary state successor that
|
|
verifies \fBp\fP.
|
|
.br
|
|
AU(p,q) : returns all states that are the root of only pathes from which \fBp\fP is true
|
|
until \fBq\fP is always true.
|
|
.br
|
|
AG(p) : returns all states that are the root of only pathes, such that \fBp\fP is always true.
|
|
|
|
.RE
|
|
|
|
.br
|
|
|
|
.SH ENVIRONMENT VARIABLES
|
|
.br
|
|
.HP
|
|
.ti 7
|
|
\fIMBK_WORK_LIB\fP gives the path for the description and the CTL file.
|
|
The default value is the current directory.
|
|
.br
|
|
.HP
|
|
.ti 7
|
|
\fIMBK_CATA_LIB\fP gives some auxiliary pathes for the descriptions and the CTL
|
|
file.
|
|
The default value is the current directory.
|
|
.SH OPTIONS
|
|
.ti 7
|
|
\-V
|
|
Sets verbose mode on. Each step of the model checking is displayed on the
|
|
standard output.
|
|
|
|
.br
|
|
\-D
|
|
Sets debug mode on. Each step of the model checking is detailed on the
|
|
standard output. In particular all states set are displayed for each
|
|
CTL sub-expression.
|
|
|
|
.br
|
|
\-B
|
|
The input file is a VHDL description using the Alliance VHDL subset
|
|
(see VBE(5) file format).
|
|
.br
|
|
.SH FSM EXAMPLE
|
|
.br
|
|
.nf
|
|
-- A multi fsm example
|
|
|
|
ENTITY example is
|
|
PORT
|
|
(
|
|
ck : in BIT;
|
|
data_in : in BIT;
|
|
reset : in BIT;
|
|
data_out : out BIT
|
|
);
|
|
END example;
|
|
|
|
|
|
ARCHITECTURE FSM OF example is
|
|
|
|
TYPE A_ETAT_TYPE IS (A_E0, A_E1);
|
|
SIGNAL A_NS, A_CS : A_ETAT_TYPE;
|
|
|
|
TYPE B_ETAT_TYPE IS (B_E0, B_E1);
|
|
SIGNAL B_NS, B_CS : B_ETAT_TYPE;
|
|
|
|
--PRAGMA CURRENT_STATE A_CS FSM_A
|
|
--PRAGMA NEXT_STATE A_NS FSM_A
|
|
--PRAGMA CLOCK ck FSM_A
|
|
--PRAGMA FIRST_STATE A_E0 FSM_A
|
|
|
|
--PRAGMA CURRENT_STATE B_CS FSM_B
|
|
--PRAGMA NEXT_STATE B_NS FSM_B
|
|
--PRAGMA CLOCK ck FSM_B
|
|
--PRAGMA FIRST_STATE B_E0 FSM_B
|
|
|
|
SIGNAL ACK, REQ, DATA_INT : BIT;
|
|
|
|
BEGIN
|
|
|
|
A_1 : PROCESS ( A_CS, ACK )
|
|
BEGIN
|
|
IF ( reset = '1' )
|
|
THEN A_NS <= A_E0;
|
|
DATA_OUT <= '0';
|
|
REQ <= '0';
|
|
ELSE
|
|
CASE A_CS is
|
|
WHEN A_E0 =>
|
|
IF ( ACK ='1') THEN A_NS <= A_E1;
|
|
ELSE A_NS <= A_E0;
|
|
END IF;
|
|
DATA_OUT <= '0';
|
|
REQ <= '1';
|
|
WHEN A_E1 =>
|
|
IF ( ACK ='1') THEN A_NS <= A_E1;
|
|
ELSE A_NS <= A_E0;
|
|
END IF;
|
|
DATA_OUT <= DATA_INT;
|
|
REQ <= '0';
|
|
END CASE;
|
|
END IF;
|
|
END PROCESS A_1;
|
|
|
|
A_2 : PROCESS( ck )
|
|
BEGIN
|
|
IF ( ck = '1' AND NOT ck'STABLE )
|
|
THEN A_CS <= A_NS;
|
|
END IF;
|
|
END PROCESS A_2;
|
|
|
|
-------
|
|
|
|
B_1 : PROCESS ( B_CS, ACK )
|
|
BEGIN
|
|
IF ( reset = '1' )
|
|
THEN B_NS <= B_E0;
|
|
DATA_INT <= '0';
|
|
ACK <= '0';
|
|
ELSE
|
|
CASE B_CS is
|
|
WHEN B_E0 =>
|
|
IF ( REQ ='1') THEN B_NS <= B_E1;
|
|
ELSE B_NS <= B_E0;
|
|
END IF;
|
|
DATA_INT <= '0';
|
|
ACK <= '0';
|
|
WHEN B_E1 =>
|
|
IF ( REQ ='1') THEN B_NS <= B_E1;
|
|
ELSE B_NS <= B_E0;
|
|
END IF;
|
|
DATA_INT <= DATA_IN;
|
|
ACK <= '1';
|
|
END CASE;
|
|
END IF;
|
|
END PROCESS B_1;
|
|
|
|
B_2 : PROCESS( ck )
|
|
BEGIN
|
|
IF ( ck = '1' AND NOT ck'STABLE )
|
|
THEN B_CS <= B_NS;
|
|
END IF;
|
|
END PROCESS B_2;
|
|
|
|
END FSM;
|
|
|
|
.br
|
|
.SH CTL EXAMPLE
|
|
.br
|
|
.nf
|
|
|
|
-- A CTL file example
|
|
|
|
TYPE A_ETAT_TYPE IS (A_E0, A_E1);
|
|
TYPE B_ETAT_TYPE IS (B_E0, B_E1);
|
|
|
|
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;
|
|
|
|
INITIAL init1 := (reset='1');
|
|
ASSUME ass1 := (reset='0');
|
|
|
|
begin
|
|
|
|
prop1 : EX( ack='1' );
|
|
prop2 : AG( req -> AF( ack ) );
|
|
prop4 : AU( req='1', ack='1');
|
|
|
|
end;
|
|
|
|
.br
|
|
.SH MOKA EXAMPLE
|
|
.br
|
|
moka -V example example
|
|
|
|
.SH SEE ALSO
|
|
.br
|
|
\fBsyf\fP (1), \fBfsp\fP (1), \fBfsm\fP (5), \fBctl\fP (5), \fBvbe(5)\fP.
|
|
|
|
.so man1/alc_bug_report.1
|
|
|