1 2(* And Delay *) 3 4val And_def = Define `And (a, b) (c, d) = (a/\c, b\/d)`;; 5 6val And_bool_def = Define `And_bool s_b s_b' = 7 !node. ((node = "out") ==> 8 (s_b' node = ((s_b "i0") /\ (s_b "i1"))))`; 9 10val And_lattice_def = Define `(And_lattice s node = 11 if (node = "i0") 12 then X 13 else if (node = "i1") then X 14 else if (node = "out") 15 then 16 And (s "i0")(s "i1") 17 else 18 X)`; 19 20val comp_list = [And_lattice_def, And_bool_def]; 21 22val a1 = (T, "i0", ``v1:bool``, 0, 1); 23val a2 = (T, "i1", ``v2:bool``, 0, 1); 24val c = (T, "out", ``(v1/\v2):bool``, 1, 2) ; 25val A = TF [a1, a2]; 26val C = TF [c]; 27 28(* Running the STE Simulator *) 29val AND_STE_IMPL1 = STE A C ``And_lattice`` comp_list true; 30 31(* when you expect a low output at the AND gate *) 32 33 (* under specification works okay *) 34val a1 = (T, "i0", ``v1:bool``, 0, 1); 35val c = (T, "out", ``F:bool``, 1, 2) ; 36val A = TF [a1]; 37val C = TF [c]; 38 39(* Running the STE Simulator *) 40val AND_STE_IMPL1 = STE A C ``And_lattice`` comp_list true; 41 42 43(* when you expect a high output at the AND gate *) 44val a1 = (T, "i0", ``v1:bool``, 0, 1); 45val a2 = (T, "i1", ``v2:bool``, 0, 1); 46val c = (T, "out", ``T:bool``, 1, 2) ; 47val A = TF [a1,a2]; 48val C = TF [c]; 49 50(* Running the STE Simulator *) 51val AND_STE_IMPL1 = STE A C ``And_lattice`` comp_list true; 52val residue = rhs(concl AND_STE_IMPL1); 53 54set_goal([], ``v1/\v2 ==> ^residue``); 55 56