Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
MOKA(1)			   CAO-VLSI Reference Manual		       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  Re-
       duced 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	reach-
       able 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).

ASIM/LIP6			August 5, 2002			       MOKA(1)

NAME | SYNOPSIS | DESCRIPTION | CTL OPERATORS | ENVIRONMENT VARIABLES | OPTIONS | FSM EXAMPLE | CTL EXAMPLE | MOKA EXAMPLE | SEE ALSO

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=moka&sektion=1&manpath=FreeBSD+12.2-RELEASE+and+Ports>

home | help