1 2(********************************************************************************************************) 3(* Function makeALU generates HOL term for transition system and init states of sync. pipelined ALU *) 4(* where the number of registers and datapath width can be varied. Used for testing RuleCheck. *) 5(* The ALU is taken from [1] Clarke et al: Model Checking, 1999 (MIT Press). *) 6(* *) 7(* state vars are: *) 8(* res = alu op result register *) 9(* op0 = alu operand reg *) 10(* op1 = alu operand reg *) 11(* reg0 = gp reg *) 12(* reg 1 = gp reg *) 13(* state vars that are inputs to the system: *) 14(* stall = whether stalling or not *) 15(* dest = dest address of res *) 16(* src0 = src add for op0 *) 17(* src1 = src add for op1 *) 18(* ctrl = op selection *) 19(********************************************************************************************************) 20 21(* Usage example (start hol including the HolCheck/examples directory, using the -I command line option) 22 Warning: this gives huge unreadable properties for aw>2 and d>4 or so 23 24app load ["holCheckLib","alu"]; 25val aw = 1; (* address space width in bits *) 26val d = 1; (* datapath width in bits *) 27val alu1 = alu.makeALU d aw; 28val alu2 = holCheckLib.holCheck alu1 handle ex => Raise ex; 29val alu3 = holCheckLib.prove_model alu2; 30val res = holCheckLib.get_results alu3; 31 32*) 33 34structure alu = 35 36struct 37 38local 39 40open Globals HolKernel Parse 41open boolSyntax bossLib pairSyntax 42open commonTools ctlSyntax holCheckLib 43 44in 45 46 47(********************************************************************************************************) 48(* generates expression for retrieving bit b of register pointed to by the register called addreg, *) 49(* where the address space is wsize bits wide *) 50(********************************************************************************************************) 51 52fun getreg addreg wsize bit = 53 let fun getreg_aux l n b = if (l=[]) then `` ^(mk_bool_var ("reg"^(int_to_string n)^"_"^b))`` 54 else ``if ^(hd l) then ^(getreg_aux (tl l) (2*n+1) b) else ^(getreg_aux (tl l) (2*n) b)``; 55 in getreg_aux (List.rev(map (fn v => mk_bool_var (addreg^"_"^v)) (List.tabulate(wsize,(fn n => (int_to_string n)))))) 0 bit end; 56 57(********************************************************************************************************) 58(* generates bitwise conjunction of equality tests for registers r1 and r2, each w bits wide *) 59(********************************************************************************************************) 60 61fun regeq r1 r2 w = 62 let val regsz = List.tabulate (w, (fn n => (int_to_string n))); 63 in boolSyntax.list_mk_conj (map (fn a => mk_eq(mk_bool_var (r1^"_"^a),mk_bool_var (r2^"_"^a))) regsz) end; 64 65(********************************************************************************************************) 66(* return HOL/CTL truth value corresponding to bit bb of the integer rr. *) 67(* useful in generating the addresses of data registers *) 68(********************************************************************************************************) 69 70(* return binary rep. of integer r1, as a list of 0's and 1's *) 71fun i2b r1 = if (Int.div(r1,2)=0) then [Int.mod(r1,2)] else (Int.mod(r1,2))::(i2b(Int.div(r1,2))); 72 73fun getbit rr bb l = 74 let val r = Option.valOf(Int.fromString rr); 75 val b = Option.valOf(Int.fromString bb); 76 val ll = (i2b r); 77 val ll = ll@List.tabulate(l - (List.length ll),(fn x => 0)); 78 in if (List.nth(ll,b)=0) then F else T handle Subscript => F end; 79 80fun getctlbit ap_ty rr bb l = 81 let val r = Option.valOf(Int.fromString rr); 82 val b = Option.valOf(Int.fromString bb); 83 val ll = (i2b r); 84 val ll = ll@List.tabulate(l - (List.length ll),(fn x => 0)); 85 in if (List.nth(ll,b)=0) then inst [alpha|->ap_ty] C_F else inst [alpha|->ap_ty] C_T 86 handle Subscript => inst [alpha|->ap_ty] C_F end; 87 88(********************************************************************************************************) 89(* Returns (thm*thm)*(ctl_wff*ctl_wff)*(string list) *) 90(* where the thms are HOL defns for the transition system and initial states of the ALU with datapath *) 91(* width d, and with an address space of aw bits. The ctl_wff's are CTL formulae expressing the *) 92(* properties that the correct destination register is updated properly (see [1] for details). The *) 93(* string list is the variable ordering with which to initialise BuDDy *) 94(********************************************************************************************************) 95 96fun makeALU d aw = 97 let 98 val datapath = List.tabulate (d, (fn n => (int_to_string n))); 99 val addpath = List.tabulate (aw, (fn n => (int_to_string n))); 100 val regnums = List.tabulate ((round(Math.pow(2.0,(Real.fromInt(aw))))), (fn n => (int_to_string n))); 101 val regfile = map (fn n => "reg"^n) regnums; 102 val dataregs = ["op0","op1","res"]@regfile; 103 val addregs = ["dest","dest_ex","dest_wb","src0","src1"]; 104 val ctrlvars = ["stall","stall_ex","stall_wb","ctrl","ctrl_ex"]; 105 val dataregvars = map mk_bool_var (List.concat (List.map (fn x => (List.map (fn y => x^"_"^y) datapath)) dataregs)); 106 val addregvars = map mk_bool_var (List.concat (List.map (fn x => (List.map (fn y => x^"_"^y) addpath)) addregs)); 107 val allvars = (dataregvars @ addregvars @ (map mk_bool_var ctrlvars)); 108 (*val state = pairSyntax.list_mk_pair allvars;*) 109 val I1 = T; 110 val bw_alu_op = map (fn n => 111 mk_disj((mk_conj(``ctrl_ex:bool``,(mk_disj((mk_bool_var ("op0_"^n)),(mk_bool_var ("op1_"^n)))))), 112 (mk_conj(``~(ctrl_ex:bool)``,(mk_neg(mk_disj((mk_bool_var ("op0_"^n)),(mk_bool_var ("op1_"^n))))))))) 113 datapath; 114 val bw_res_trans = map (fn a => mk_eq((mk_bool_var ("res_"^a^"'")),mk_cond(``~stall_ex:bool``, 115 (List.nth(bw_alu_op, (string_to_int a))), 116 (mk_bool_var ("res_"^a))))) datapath; 117 val bw_op0_trans = map (fn a => ``^(mk_bool_var ("op0_"^a^"'")) = if (~stall_ex /\ (^(regeq "dest_ex" "src0" aw))) 118 then ^(List.nth(bw_alu_op, (string_to_int a))) 119 else (if stall_wb 120 then (^(getreg "src0" aw a)) 121 else (if (^(regeq "dest_wb" "src0" aw)) 122 then (^(mk_bool_var ("res_"^a))) 123 else (^(getreg "src0" aw a))))``) datapath; 124 val bw_op1_trans = map (fn a => ``^(mk_bool_var ("op1_"^a^"'")) = if (~stall_ex /\ (^(regeq "dest_ex" "src1" aw))) 125 then ^(List.nth(bw_alu_op, (string_to_int a))) 126 else (if stall_wb 127 then (^(getreg "src1" aw a)) 128 else (if (^(regeq "dest_wb" "src1" aw)) 129 then (^(mk_bool_var ("res_"^a))) 130 else (^(getreg "src1" aw a))))``) datapath; 131 val bw_reg_trans = map (fn n => 132 (map (fn a => mk_eq(mk_bool_var ("reg"^n^"_"^a^"'"), 133 mk_cond(``stall_wb:bool``,mk_bool_var ("reg"^n^"_"^a), 134 mk_cond((boolSyntax.list_mk_conj(List.map 135 (fn b => mk_eq(mk_bool_var("dest_wb_"^b), 136 (getbit n b aw))) addpath)), 137 mk_bool_var("res_"^a), 138 mk_bool_var("reg"^n^"_"^a) )))) datapath)) regnums; 139 val bw_reg_trans = map list_mk_conj bw_reg_trans; 140 val bw_dest_trans = map (fn n => list_mk_conj(map (fn (x,y) => mk_eq(mk_bool_var(x^"_"^n^"'"), 141 mk_bool_var(y^"_"^n))) [("dest_wb","dest_ex"), 142 ("dest_ex","dest")])) addpath; 143 val R1 = list_mk_conj (bw_res_trans @ bw_op0_trans @ bw_op1_trans @ bw_reg_trans @ bw_dest_trans 144 @ [(``stall_ex':bool = stall:bool``),(``stall_wb':bool=stall_ex:bool``), (``ctrl_ex':bool=ctrl:bool``)]) 145 val T1 = [(".",R1)]; 146 147 (* define properties *) 148 infixr 5 C_AND infixr 5 C_OR infixr 2 C_IMP infix C_IFF; 149 val state = ksTools.mk_state I1 T1 150 151 fun alu_AP s = C_AP state (mk_bool_var s) 152 val ap_ty = (type_of state) --> bool 153 val bw_op0_defs = List.map (fn b => list_C_OR 154 (List.map (fn x => (C_AX(C_AX(alu_AP ("reg"^x^"_"^b)))) C_AND 155 (list_C_AND (List.map (fn y => (alu_AP ("src0"^"_"^y)) C_IFF (getctlbit ap_ty x y aw)) 156 addpath))) regnums)) datapath; 157 val bw_op1_defs = List.map (fn b => list_C_OR 158 (List.map (fn x => (C_AX(C_AX(alu_AP ("reg"^x^"_"^b)))) C_AND 159 (list_C_AND (List.map (fn y=>((alu_AP ("src1"^"_"^y)) C_IFF (getctlbit ap_ty x y aw))) 160 addpath))) regnums)) datapath; 161 val bw_res_defs = List.map (fn b => list_C_OR(map (fn x => (C_AX(C_AX(C_AX(alu_AP ("reg"^x^"_"^b))))) C_AND 162 (list_C_AND(List.map (fn y => ((alu_AP ("dest"^"_"^y)) C_IFF (getctlbit ap_ty x y aw))) 163 addpath))) regnums)) datapath; 164 val bw_ctl_alu_op_defs = map (fn (x,y) => ((alu_AP ("ctrl")) C_AND (x C_OR y)) C_OR ((C_NOT(alu_AP ("ctrl"))) C_AND 165 (C_NOT( x C_OR y)))) 166 (ListPair.zip(bw_op0_defs,bw_op1_defs)); 167 168 val bw_prop1 = map (fn (x,y) => (C_AG((C_NOT(alu_AP ("stall"))) C_IMP (((x C_IFF y)))))) 169 (ListPair.zip(bw_ctl_alu_op_defs,bw_res_defs)) 170 val bw_prop1 = List.map (fn (p,n) => ("p1_"^(int_to_string n),p)) (ListPair.zip(bw_prop1,List.tabulate(List.length bw_prop1,I))) 171 172 val bw_prop2 = map (fn b => list_C_AND(map 173 (fn rg => 174 (C_AG( (alu_AP ("stall")) C_IMP 175 (list_C_AND(map 176 (fn a =>C_NOT((alu_AP ("dest"^"_"^a)) C_IFF (getctlbit ap_ty rg a aw))) 177 addpath)) C_OR 178 (((C_AX(C_AX(alu_AP ("reg"^rg^"_"^b)))) C_IFF 179 (C_AX(C_AX(C_AX(alu_AP ("reg"^rg^"_"^b)))))))))) 180 regnums)) datapath; 181 val bw_prop2 = List.map (fn (p,n) => ("p2_"^(int_to_string n),p)) (ListPair.zip(bw_prop2,List.tabulate(List.length bw_prop2,I))) 182 183 fun makeBddMap d aw = 184 let 185 val resv = map (fn v => ("res_"^v,"res_"^v^"'")) datapath; 186 val op0v = map (fn v => ("op0_"^v,"op0_"^v^"'")) datapath; 187 val op1v = map (fn v => ("op1_"^v,"op1_"^v^"'")) datapath; 188 val destv =List.concat(List.concat (map (fn v => map (fn a => [v^a,v^a^"'"]) addpath) ["dest_","dest_ex_","dest_wb_"])); 189 val src0v = map (fn v => ("src0_"^v,"src0_"^v^"'")) addpath; 190 val src1v = map (fn v => ("src1_"^v,"src1_"^v^"'")) addpath; 191 val stallv = ["stall","stall'","stall_ex","stall_ex'","stall_wb","stall_wb'"]; 192 val ctrlv = ["ctrl","ctrl'","ctrl_ex","ctrl_ex'"]; 193 val regv = (map (fn rg => rev(map (fn d => ("reg"^rg^"_"^d,"reg"^rg^"_"^d^"'")) datapath)) regnums); 194 fun interleave l1 l2 = List.concat(map (fn ((x,x'),(y,y')) => [x,x',y,y']) (ListPair.zip(l1,l2))); 195 fun stdest l1 l2 = if (l1=[]) then [] else List.take(l1,2)@List.take(l2,aw*2)@(stdest (List.drop(l1,2)) (List.drop(l2,aw*2))) ; 196 fun geninter L = (if (hd(L)=[]) then [] 197 else (List.concat(map (fn l => [fst(hd(l)),snd(hd(l))] ) L))::(geninter(map (fn l => tl(l)) L))); 198 in (interleave src0v src1v) @ (stdest stallv destv) @ ctrlv @ 199 (List.concat(geninter ([(rev op0v)]@[(rev op1v)]@(regv)@[(rev resv)]))) end 200 val bvm = makeBddMap d aw; 201 in ((set_init I1) o (set_trans T1) o (set_flag_ric true) o (set_name "alu") o (set_vord bvm)o (set_state state) o 202 (set_props(bw_prop1@bw_prop2))) empty_model end; 203 204 205 206 207end 208end 209