GSP
Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Support
Contact Us
Online Help
Handbooks
Domain Status
Man Pages

FAQ
Virtual Servers
Pricing
Billing
Technical

Network
Facilities
Connectivity
Topology Map

Miscellaneous
Server Agreement
Year 2038
Credits
 

USA Flag

 

 

Man Pages


Manual Reference Pages  -  CTL (5)

NAME

ctl - Control Temporal Logic file format.

[Include document man1/alc_origin.1]

CONTENTS

Description
Example
See Also

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)

[Include document man1/alc_bug_report.1]

Search for    or go to Top of page |  Section 5 |  Main Index


ASIM/LIP6 CTL (5) August 5, 2002

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with manServer 1.07.