NAME¶
ctl - Control Temporal Logic file format.
ORIGIN¶
This software belongs to the ALLIANCE CAD SYSTEM developed by the ASIM team at
LIP6 laboratory of Université Pierre et Marie CURIE, in Paris,
France.
Web :
http://asim.lip6.fr/recherche/alliance/
E-mail :
alliance-users@asim.lip6.fr
DESCRIPTION¶
This document describes the CTL file format used by
moka(1) for model
checking of finite states machine description.
This CTL file format subset is defined to enable classical CTL formulae
description.
A CTL file is made of two parts: a declaration part and a formulae statement
part.
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
moka(1) during the model
checking.
The formulae statement part described all the CTL formulae that have to be
verified.
All boolean and relational 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
'<=>'.
EXAMPLE¶
-- 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.
RESET_COND init1 := (reset='1');
-- It is also possible to describe the first state
-- with the INITIAL keywork, as follows:
--
-- INITIAL init1 := ((A_CS=A_E0) AND (B_CS=B_E0));
--
-- formulae description statement part
begin
prop1 : EX( ack='1' );
prop2 : AG( req -> AF( ack ) );
prop4 : AU( req='1', ack='1');
end;
SEE ALSO¶
moka(1)
BUG REPORT¶
This tool is under development at the
ASIM department of the
LIP6
laboratory.
We need your feedback to improve documentation and tools.