CTL(5)

💖 ctl — the CTL file format, bestie edition 💖

okay so welcome to the CTL(5) girlies, this is the manual page for the CTL file format of the ASIM/LIP6/CAO-VLSI lab ✨

---

🌸 ORIGIN 🌸

This software is part of the ALLIANCE CAD SYSTEM, and it was cooked up by the ASIM team at the LIP6 laboratory of Université Pierre et Marie CURIE, in Paris, France 🇫🇷 (yes, the Paris, the vibes are immaculate).

• Web : http://asim.lip6.fr/recherche/alliance/
• E-mail : alliance-users@asim.lip6.fr

---

✨ DESCRIPTION ✨

This doc is the whole rundown on the CTL file format that moka(1) uses 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, and honestly both of them eat:

1. a declaration part
2. 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. no notes, it just does.

All boolean and relational VHDL operators are supported (see vbe(5)) and also the 8 CTL operators — say it with me, bestie:

• AF
• AG
• AX
• AU
• EF
• EG
• EX
• EU

The CTL file format support also the imply boolean operator '->' and the equivalence operator '<=>'. iconic behaviour fr fr 🌈

---

🎀 EXAMPLE 🎀

this is the whole thing verbatim, don't skip, she's long but she's worth it

--  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;

⚠️ be careful, bestie: the assumption condition is not applied to the initial conditions. that part is literally spelled out in the example comments and it is NOT a drill 💀

---

🦋 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. so like… tell them things 🫶

---

and that's the whole page, no cap 💜 mwah, this was ASIM/LIP6, dated August 5, 2002 — yes she's an elder but she's still serving CTL(5) energy, and honestly? periodt. ✨👑🎀