MOKA(1) | CAO-VLSI Reference Manual | MOKA(1) |
NAME¶
- MOKA - Model checker ancestor
ORIGIN¶
This software belongs to the ALLIANCE CAD SYSTEM developed by the ASIM team at LIP6 laboratory of Université Pierre et Marie CURIE, in Paris, France.SYNOPSIS¶
- moka [-VDB] fsm_filename ctl_filename
-
DESCRIPTION¶
moka is a CTL model checker.CTL OPERATORS¶
For each CTL sub-expression moka 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).ENVIRONMENT VARIABLES¶
MBK_WORK_LIB gives the path for the description and the
CTL file. The default value is the current directory.
MBK_CATA_LIB gives some auxiliary pathes for the
descriptions and the CTL file. The default value is the current
directory.
OPTIONS¶
-V Sets verbose mode on. Each step of the model checking is displayed on the standard output.FSM EXAMPLE¶
-- 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;
CTL EXAMPLE¶
-- 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; RESET_COND init1 := (reset='1'); ASSUME ass1 := (reset='0'); begin prop1 : EX( ack='1' ); prop2 : AG( req -> AF( ack ) ); prop4 : AU( req='1', ack='1'); end;
MOKA EXAMPLE¶
moka -V example exampleSEE ALSO¶
syf (1), fsp (1), fsm (5), ctl (5), vbe(5).
BUG REPORT¶
This tool is under development at the ASIM department of the LIP6 laboratory.August 5, 2002 | ASIM/LIP6 |