From 08440e5dbd9447a83961ededc01b9f43d3fa7543 Mon Sep 17 00:00:00 2001 From: Ludovic Jacomme Date: Mon, 5 Aug 2002 13:36:08 +0000 Subject: [PATCH] Le man de moka !!! --- alliance/src/mocha/Makefile.am | 2 +- alliance/src/mocha/configure.in | 1 + alliance/src/mocha/man1/Makefile.am | 2 + alliance/src/mocha/man1/moka.1 | 195 ++++++++++++++++++++++++++++ 4 files changed, 199 insertions(+), 1 deletion(-) create mode 100644 alliance/src/mocha/man1/Makefile.am create mode 100644 alliance/src/mocha/man1/moka.1 diff --git a/alliance/src/mocha/Makefile.am b/alliance/src/mocha/Makefile.am index af437a64..5fcaa0d3 100644 --- a/alliance/src/mocha/Makefile.am +++ b/alliance/src/mocha/Makefile.am @@ -1 +1 @@ -SUBDIRS = src +SUBDIRS = src man1 diff --git a/alliance/src/mocha/configure.in b/alliance/src/mocha/configure.in index 1ad62753..7f429c99 100644 --- a/alliance/src/mocha/configure.in +++ b/alliance/src/mocha/configure.in @@ -28,5 +28,6 @@ AM_ALLIANCE AC_OUTPUT([ Makefile +man1/Makefile src/Makefile ]) diff --git a/alliance/src/mocha/man1/Makefile.am b/alliance/src/mocha/man1/Makefile.am new file mode 100644 index 00000000..a0f89b3c --- /dev/null +++ b/alliance/src/mocha/man1/Makefile.am @@ -0,0 +1,2 @@ +man_MANS = moka.1 +EXTRA_DIST = $(man_MANS) diff --git a/alliance/src/mocha/man1/moka.1 b/alliance/src/mocha/man1/moka.1 new file mode 100644 index 00000000..2698ee76 --- /dev/null +++ b/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 +