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