From c8987e53fbc2cf252918a0409e6cb1c2f6bae300 Mon Sep 17 00:00:00 2001 From: Ludovic Jacomme Date: Mon, 5 Aug 2002 13:35:40 +0000 Subject: [PATCH] Le man de CTL --- alliance/src/ctl/Makefile.am | 2 +- alliance/src/ctl/configure.in | 3 +- alliance/src/ctl/man5/Makefile.am | 2 + alliance/src/ctl/man5/ctl.5 | 86 +++++++++++++++++++++++++++++++ 4 files changed, 91 insertions(+), 2 deletions(-) create mode 100644 alliance/src/ctl/man5/Makefile.am create mode 100644 alliance/src/ctl/man5/ctl.5 diff --git a/alliance/src/ctl/Makefile.am b/alliance/src/ctl/Makefile.am index af437a64..d78b6217 100644 --- a/alliance/src/ctl/Makefile.am +++ b/alliance/src/ctl/Makefile.am @@ -1 +1 @@ -SUBDIRS = src +SUBDIRS = src man5 diff --git a/alliance/src/ctl/configure.in b/alliance/src/ctl/configure.in index 2b0da2d1..d18e9194 100644 --- a/alliance/src/ctl/configure.in +++ b/alliance/src/ctl/configure.in @@ -26,7 +26,7 @@ dnl Almost ten years since I wrote this stuff, I just can't dnl believe it dnl Date : 01/02/2002 dnl Author : Frederic Petrot -dnl $Id: configure.in,v 1.1 2002/04/18 15:24:28 ludo Exp $ +dnl $Id: configure.in,v 1.2 2002/08/05 13:35:35 ludo Exp $ dnl dnl AC_INIT(src/ctl.h) @@ -41,5 +41,6 @@ AM_ALLIANCE AC_OUTPUT([ Makefile +man5/Makefile src/Makefile ]) diff --git a/alliance/src/ctl/man5/Makefile.am b/alliance/src/ctl/man5/Makefile.am new file mode 100644 index 00000000..ec8b7934 --- /dev/null +++ b/alliance/src/ctl/man5/Makefile.am @@ -0,0 +1,2 @@ +man_MANS = ctl.5 +EXTRA_DIST = $(man_MANS) diff --git a/alliance/src/ctl/man5/ctl.5 b/alliance/src/ctl/man5/ctl.5 new file mode 100644 index 00000000..f4e71ec2 --- /dev/null +++ b/alliance/src/ctl/man5/ctl.5 @@ -0,0 +1,86 @@ +.TH CTL 5 "August 5, 2002" "ASIM/LIP6" "CTL file format of ASIM/LIP6/CAO-VLSI lab." + +.SH NAME +.PP +\fBctl\fP - Control Temporal Logic file format. + +.so man1/alc_origin.1 +.SH DESCRIPTION +.PP +This document describes the CTL file format used by \fBmoka\fP(1) for model checking +of finite states machine description. + +.br +This CTL file format subset is defined to enable classical CTL formulae description. +.br +A CTL file is made of two parts: a declaration part and a formulae statement part. + +.br +The declaration part described types, constants, macros and all variables used in CTL formulae. +It also describes assumption conditions and initial conditions that have to be applied +by \fBmoka\fP(1) during the model checking. + +.br +The formulae statement part described all the CTL formulae that have to be verified. + +.br +All boolean VHDL operators are supported (see vbe(5)) and also the 8 CTL operators +AF, AG, AX, AU, EF, EG, EX and EU. The CTL file format support also the imply +boolean operator '->' and the equivalence operator '<=>'. +.br +.SH EXAMPLE +.PP +.nf + + +-- user type definition + + TYPE A_ETAT_TYPE IS (A_E0, A_E1); + TYPE B_ETAT_TYPE IS (B_E0, B_E1); + +-- variables definition + + 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; + +-- example of a macros definition + + DEFINE def1 : BOOLEAN := ack='1'; + +-- the assigned value can be a constant + + DEFINE c1 : BIT := '1'; + +-- the assumption condition + + ASSUME ass1 := (reset='0'); + +-- the initial reset condition +-- be careful, the assumption condition is not applied +-- to the initial conditions. + + INITIAL init1 := (reset='1'); + +-- formulae description statement part + +begin + + prop1 : EX( ack='1' ); + prop2 : AG( req -> AF( ack ) ); + prop4 : AU( req='1', ack='1'); + +end; + +.SH SEE ALSO +.PP +\fBmoka\fP(1) + +.so man1/alc_bug_report.1 +