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