(************************************************************
 *                      IMITATOR MODEL                      
 *
 * Modeling of the circuit described in "Verification of timed circuits with symbolic delays" (Clariso -- Cortadella)
 *
 * Description     : A flip-flop circuit made of 4 gates
 * Correctness     : TODO
 * Source          : "Verification of timed circuits with symbolic delays" (Clariso -- Cortadella); Design Automation Conference, 2004. Proceedings of the ASP-DAC 2004. Asia and South Pacific; DOI: 10.1109/ASPDAC.2004.1337668
 * Author          : Roberto Clariso and Jordi Cortadella
 * Modeling        : Étienne André and Laurent Fribourg
 * Input by        : Étienne André
 *
 * Created         : 2007/11
 * Last modified   : 2020/08/14
 *
 * IMITATOR version: 3.0
 ************************************************************)
 
(*
(***** BAD ONE *****)
	& tHI = 20
	& tLO = 15
	& tSetup = 10
	& tHold = 15
	& dG1_l = 1
	& dG1_u = 1
	& dG2_l = 8
 	& dG2_u = 10
	& dG3_l = 5
 	& dG3_u = 6
	& dG4_l = 3
	& dG4_u = 5
*)



(* ----- IJFCS [ACEF09] ----- *)

property := #synth IM(
	& tHI    = 24
	& tLO    = 15
	& tSetup = 10
	& tHold  = 17
	& dG1_l  = 7
	& dG1_u  = 7
	& dG2_l  = 5
	& dG2_u  = 6
	& dG3_l  = 8
	& dG3_u  = 10
	& dG4_l  = 3
	& dG4_u  = 7
);

(*
-- 	& tHI    = 24
-- 	& tLO    = 15
-- 	& tSetup = 10
-- 	& tHold  = 17
-- 	& dG1_l  = 7
-- 	& dG1_u  = 7
-- 	& dG2_l  = 5
-- 	& dG2_u  = 6
-- 	& dG3_l  = 8
-- 	& dG3_u  = 16.9
-- 	& dG4_l  = 3
-- 	& dG4_u  = 7.8
*)