1(* Unit delay 2-to-1 two bit MUX *)
2
3val fs = FULL_SIMP_TAC std_ss;
4val fl = FULL_SIMP_TAC list_ss;
5val fw = FULL_SIMP_TAC (srw_ss());
6
7(* Basic circuit functions defined on a domain of lattice values *)
8val Or_def = Define `Or (a, b) (c, d) = (a\/c, b/\d)`;;
9
10val Not_def = Define `Not (a:bool, b:bool) = (b, a)`;;
11
12val And_def = Define `And (a, b) (c, d) = (a/\c, b\/d)`;;
13
14(* Unit delay 2-to-1 two bit MUX ---  lattice model *)
15val Mux_lattice_def =
16    Define `(Mux_lattice s node =
17             if (node = "a0") then X
18             else if (node = "a1") then X
19                  else if (node = "b0") then X
20                       else if (node = "b1") then X
21                            else if (node = "ctrl") then X
22                                 else
23                                     if (node = "out0")
24                                         then
25                                             Or
26                                             (And (s "a0")(s "ctrl"))
27                                             (And (s "b0")(Not(s "ctrl")))
28                                     else
29                                         if (node = "out1")
30                                             then
31                                                 Or
32                                                 (And (s "a1")(s "ctrl"))
33                                                 (And (s "b1")(Not(s "ctrl")))
34                                         else X)`;
35
36(* Unit delay 2-to-1 MUX Boolean model *)
37val Mux_bool_def = Define `Mux_bool s_b s_b' =
38    !node.
39    (if (node = "out0") then
40         if (s_b "ctrl") then
41             (s_b' "out0" = s_b "a0")
42         else (s_b' "out0" = s_b "b0")
43     else if (node = "out1") then
44         if (s_b "ctrl") then
45             (s_b' "out1" = s_b "a1")
46         else (s_b' "out1" = s_b "b1")
47          else T)`;
48
49
50val comp_list = [Mux_lattice_def, Or_def, And_def, Not_def];
51
52(* prove that it is okay to relate the two models for MUX *)
53val MUX_OK =
54    store_thm("MUX_OK",
55              ``Okay (Mux_lattice, Mux_bool)``,
56              FULL_SIMP_TAC std_ss [Okay_def, Mux_lattice_def, Or_def,
57                                    Mux_bool_def, And_def, Not_def,
58                                    extended_drop_state_def, leq_def,
59                                    leq_state_def]
60              THEN REPEAT STRIP_TAC
61              THEN REPEAT COND_CASES_TAC
62              THENL [PROVE_TAC [lattice_X1_lemma],
63                     PROVE_TAC [lattice_X1_lemma],
64                     PROVE_TAC [lattice_X1_lemma],
65                     PROVE_TAC [lattice_X1_lemma],
66                     PROVE_TAC [lattice_X1_lemma],
67                     FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"out0"``)
68                         THEN fw []
69                         THEN POP_ASSUM MP_TAC
70                            THEN COND_CASES_TAC
71                            THENL [fl [] THEN Cases_on `s_b "a0"`
72                                   THEN Cases_on `s_b "b0"`
73                                   THEN Cases_on `s_b' "out0"`
74                                   THEN fs [drop_def, One_def, Zero_def,
75                                            X_def, Top_def, lub_def,
76                                            Or_def, And_def, Not_def],
77                                   Cases_on `s_b "a0"`
78                                   THEN Cases_on `s_b "b0"`
79                                   THEN Cases_on `s_b' "out0"`
80                                   THEN fs [drop_def, One_def, Zero_def,
81                                            X_def, Top_def, lub_def,
82                                            Or_def, And_def, Not_def]],
83                     FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"out1"``)
84                     THEN fw []
85                     THEN POP_ASSUM MP_TAC THEN (REPEAT COND_CASES_TAC)
86                     THENL [fl [] THEN Cases_on `s_b "a1"`
87                            THEN Cases_on `s_b "b1"`
88                            THEN Cases_on `s_b' "out1"`
89                            THEN fs [drop_def, One_def, Zero_def,
90                                     X_def, Top_def, lub_def,
91                                     Or_def, And_def, Not_def],
92                            fl [] THEN Cases_on `s_b "a1"`
93                            THEN Cases_on `s_b "b1"`
94                            THEN Cases_on `s_b' "out1"`
95                            THEN fs [drop_def, One_def, Zero_def,
96                                     X_def, Top_def, lub_def,
97                                     Or_def, And_def, Not_def]],
98                     PROVE_TAC [lattice_X1_lemma]]);
99
100(* prove that the MUX circuit is monotonic *)
101val MUX_MONOTONIC =
102    store_thm("MUX_MONOTONIC", ``Monotonic Mux_lattice``,
103              FULL_SIMP_TAC std_ss [Monotonic_def,
104                                    Mux_lattice_def,
105                                    Or_def,
106                                    And_def, Not_def,
107                                    extended_drop_state_def,
108                                    leq_state_def]
109              THEN REPEAT STRIP_TAC
110              THEN REPEAT COND_CASES_TAC
111              THEN fs [leq_def, lub_def, X_def]
112              THENL [REPEAT (POP_ASSUM MP_TAC)
113                     THEN CONV_TAC(TOP_DEPTH_CONV(stringLib.string_EQ_CONV))
114                     THEN RW_TAC std_ss [],
115                     FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a0"``)
116                     THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"ctrl"``)
117                     THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"b0"``)
118                     THEN Cases_on `s "a0"` THEN Cases_on `s' "a0"`
119                     THEN Cases_on `s "b0"` THEN Cases_on `s' "b0"`
120                     THEN Cases_on `s "ctrl"` THEN Cases_on `s' "ctrl"`
121                     THEN fs [Not_def, And_def, Or_def, lub_def]
122                     THEN RW_TAC std_ss [] THEN
123                     EQ_TAC THEN REPEAT STRIP_TAC THEN fs [],
124                     FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a1"``)
125                     THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"ctrl"``)
126                     THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"b1"``)
127                     THEN Cases_on `s "a1"` THEN Cases_on `s' "a1"`
128                     THEN Cases_on `s "b1"` THEN Cases_on `s' "b1"`
129                     THEN Cases_on `s "ctrl"` THEN Cases_on `s' "ctrl"`
130                     THEN fs [Not_def, And_def, Or_def, lub_def]
131                     THEN RW_TAC std_ss [] THEN
132                     EQ_TAC THEN REPEAT STRIP_TAC THEN fs []]);
133
134
135
136(*********************** E X A M P L E S *******************************)
137
138
139(* Example I *)
140val a0 = (T, "a0", T, 0, 1);
141val a1 = (T, "a1", T, 0, 1);
142val b0 = (T, "b0", F, 0, 1);
143val b1 = (T, "b1", F, 0, 1);
144
145val ctrl = (T, "ctrl", T, 0, 1);
146
147val out0 = (T, "out0", T, 1, 2);
148val out1 = (T, "out1", T, 1, 2);
149
150val A  =  TF [ctrl, a0, a1, b0, b1];
151val C  =  TF [out0, out1] ;
152
153(* Running the STE simulator *)
154val MUX_STE_IMPL1 = STE A C ``Mux_lattice`` comp_list true;
155
156(* STE TO BOOL *)
157val MUX_STE_BOOL1 =
158    STE_TO_BOOL A C ``Mux_lattice`` ``Mux_bool``
159    MUX_OK MUX_MONOTONIC MUX_STE_IMPL1;
160
161CONV_RULE(EVAL) MUX_STE_BOOL1;
162
163(* Example II *)
164
165val a0 = (T, "a0", ``va0:bool``, 0, 1);
166val a1 = (T, "a1", ``va1:bool``, 0, 1);
167val b0 = (T, "b0", ``vb0:bool``, 0, 1);
168val b1 = (T, "b1", ``vb1:bool``, 0, 1);
169val ctrl = (T, "ctrl", T, 0, 1);
170val out0 = (T, "out0", ``va0:bool``, 1, 2);
171val out1 = (T, "out1", ``va1:bool``, 1, 2);
172val A  =  TF [ctrl,a0,a1,b0,b1];
173val C  =  TF [out0, out1] ;
174
175(* Running the STE simulator *)
176val MUX_STE_IMPL2 = STE A C ``Mux_lattice`` comp_list true;
177
178(* STE TO BOOL *)
179val MUX_STE_BOOL2 =
180    STE_TO_BOOL A C ``Mux_lattice`` ``Mux_bool``
181    MUX_OK MUX_MONOTONIC MUX_STE_IMPL2;
182
183CONV_RULE(EVAL) MUX_STE_BOOL2;
184
185
186(* Example III *)
187
188val a0 = (T, "a0", ``va0:bool``, 0, 1);
189val a1 = (T, "a1", ``va1:bool``, 0, 1);
190val b0 = (T, "b0", ``vb0:bool``, 0, 1);
191val b1 = (T, "b1", ``vb1:bool``, 0, 1);
192val ctrl = (T, "ctrl", ``ctrl:bool``, 0, 1);
193
194val out0 = (T, "out0", ``(va0 /\ ctrl) \/ (vb0 /\ (~ctrl))``, 1, 2);
195val out1 = (T, "out1", ``(va1 /\ ctrl) \/ (vb1 /\ (~ctrl))``, 1, 2);
196val A  =  TF [ctrl,a0,a1,b0,b1] ;
197val C  =  TF [out0, out1];
198val A  =  TF [ctrl,a0,a1,b0,b1];
199val C  =  TF [out0, out1] ;
200
201(* Running the STE simulator *)
202val MUX_STE_IMPL3 = STE A C ``Mux_lattice`` comp_list true;
203
204(* STE TO BOOL *)
205val MUX_STE_BOOL3 =
206    STE_TO_BOOL A C ``Mux_lattice`` ``Mux_bool``
207    MUX_OK MUX_MONOTONIC MUX_STE_IMPL3;
208
209CONV_RULE(EVAL) MUX_STE_BOOL3;
210