Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
CTL(5)		  CTL file format of ASIM/LIP6/CAO-VLSI	lab.		CTL(5)

NAME
       ctl - Control Temporal Logic file format.

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	 vari-
       ables  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	equiv-
       alence 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)

ASIM/LIP6			August 5, 2002				CTL(5)

NAME | DESCRIPTION | EXAMPLE | SEE ALSO

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=ctl&sektion=5&manpath=FreeBSD+12.2-RELEASE+and+Ports>

home | help