---
name: "moka"
section: "1"
platform: "linux"
package: "alliance"
version: "5.1.1-3"
release: "Debian 10 (Buster)"
platforms: ["linux"]
url: "https://new.carta.tech/moka"
---

# moka(1)

## NAME

- MOKA - Model checker ancestor

  ## SYNOPSIS

- ***moka \[-VDB\] fsm\_filename ctl\_filename***

  ## DESCRIPTION

**moka** ***is a CTL model checker.***\

***Made to run on FSM or RTL descriptions,*** **moka** ***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*** **moka** ***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.***\
 ***First of all*** **moka** ***build the fonction transition of the FSM using*** ***a Reduced Ordered Binary Decision Diagrams representation.***\
 ***It then applies the initial conditions to find the first state (keyword INITIAL*** ***and/or RESET\_COND in the CTL(5) file format).***\
 ***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).***\
 **moka** ***finally verifies one by one each CTL formulae.*** ***(see CTL(5) for CTL file format details).***

## 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).***\
 ***CTL operators :***

***EX(p) : returns all states which have almost one primary state successor that*** ***verifies*** **p*****.***\
 ***EU(p,q) : returns all states that are the root of almost one path, such that*** **p** ***is true***  ***until*** **q** ***is always true.***\
 ***EG(p) : returns all states that are the root of almost one path, such that*** **p** ***is always true.***\
 ***AX(p) : returns all states which have all their primary state successor that*** ***verifies*** **p*****.***\
 ***AU(p,q) : returns all states that are the root of only pathes from which*** **p** ***is true***  ***until*** **q** ***is always true.***\
 ***AG(p) : returns all states that are the root of only pathes, such that*** **p** ***is always true.***

## 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.***

***-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.***

***-B*** ***The input file is a VHDL description using the Alliance VHDL subset*** ***(see VBE(5) file format).***\

## 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 example***

## SEE ALSO

 **syf** ***(1),*** **fsp** ***(1),*** **fsm** ***(5),*** **ctl** ***(5),*** **[vbe(5)](/vbe/5.md)*****.***