Le man de moka !!!

alliance/src/mocha/Makefile.am

@@ -1 +1 @@
-SUBDIRS = src
+SUBDIRS = src man1

alliance/src/mocha/configure.in

@@ -28,5 +28,6 @@ AM_ALLIANCE
 
 AC_OUTPUT([
 Makefile
+man1/Makefile
 src/Makefile
 ])

alliance/src/mocha/man1/Makefile.am

@@ -0,0 +1,2 @@
+man_MANS  = moka.1
+EXTRA_DIST = $(man_MANS)

alliance/src/mocha/man1/moka.1

@@ -0,0 +1,195 @@
+.\" @(#) 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), FSM(5), VBE(5) ).
+\fBmoka\fP uses a Reduced Ordered Binary Decision Diagrams representation and 
+verifies CTL formulae  (see CTL(5) for CTL file format details).
+
+.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.
+
+.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
+