CTL(5)

💅 CTL — ctl(5), the manual page for the CTL file format

okay so real quick before we dive in: this is ctl(5), section 5 of the manual — aka the page about the CTL file format itself. Buckle up bestie, we're learning a file format today 🎀

---

✨ NAME ✨

ctl — the Control Temporal Logic file format. that's it, that's the name, and honestly? iconic. 🔥

---

🌸 ORIGIN 🌸

okay so this software belongs to the ALLIANCE CAD SYSTEM, which was developed by the ASIM team over at the LIP6 laboratory of Université Pierre et Marie CURIE, in Paris, France. oui oui, Paris 💖

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

like, actual humans to email. use it, they're nice 💌

---

🦋 DESCRIPTION 🦋

So this doc describes the CTL file format, which moka(1) uses for model checking of finite states machine description. That's the whole vibe — moka reads a CTL file, and the file says "hey, check these properties for me."

This CTL file format is a subset — and that subset is specifically defined to enable classical CTL formulae description. Lowkey everything you need, nothing you don't 💅

A CTL file is made of two parts: a declaration part and a formulae statement part.

🎀 the declaration part

The declaration part describes types, constants, macros and all variables used in CTL formulae. It also describes the assumption conditions and initial conditions that have to be applied by moka(1) during the model checking. so it's giving "here's the setup, here's the ground rules" energy.

⭐ the formulae statement part

The formulae statement part describes all the CTL formulae that have to be verified. that's the part where you're like "okay moka, prove it" 🙈

🔥 the operators (this is the fun part)

All boolean and relational VHDL operators are supported — go check vbe(5) for those, bestie — and also the 8 CTL operators:

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

The CTL file format also supports the imply boolean operator '->' and the equivalence operator '<=>'. yes, both. no cap. 🫶

---

🌈 EXAMPLE 🌈

here's a whole example, copy-paste energy:

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

⚠️ ok bestie, do not miss this one: be careful, the assumption condition is not applied to the initial conditions. like, that's a whole gotcha right there 😭 the note lives in the example above, but I'm putting it in a big pink box so you actually see it.

Also peep that you can describe the first state with the INITIAL keyword too — there's a commented-out example up there showing exactly how. (the original page spells it "keywork" in that comment, so I kept it verbatim, don't come for me 💀)

---

👑 SEE ALSO 👑

• moka(1) — go read this one next fr fr

---

💀 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… actually tell them?? they're literally asking 🥺

---

and that's the whole page bestie ✨ you're now a CTL file format expert, periodt 💅

This masterpiece of a manpage came to you from ASIM/LIP6, dated August 5, 2002 — drink some water, go write some formulae, and stan moka(1) 🫶💖