1(*****************************************************************************) 2(* High level (TFL) specification and implementation of factorial *) 3(* using ``:word32`` instead of ``:num`` *) 4(*****************************************************************************) 5 6quietdec := true; 7 8loadPath := "../" :: "../dff/" :: !loadPath; 9app load 10 ["compileTheory","compile","metisLib", "wordsLib", "dffTheory","vsynth"]; 11open compile metisLib wordsTheory wordsLib; 12open arithmeticTheory pairLib pairTheory PairRules combinTheory 13 devTheory composeTheory compileTheory compile vsynth dffTheory; 14infixr 3 THENR; 15infixr 3 ORELSER; 16numLib.prefer_num(); 17 18quietdec := false; 19 20 21(*****************************************************************************) 22(* Start new theory "Fact32" *) 23(*****************************************************************************) 24 25val _ = new_theory "Fact32"; 26 27(*---------------------------------------------------------------------------*) 28(* Tell hwDefine about how to deal with "predecessor-based" recursions on *) 29(* words. Allows factorial and other iterations to be dealt with. *) 30(*---------------------------------------------------------------------------*) 31 32add_combinational ["MOD","DIV"]; 33add_combinational ["word_add","word_sub"]; 34add_combinational ["BITS","w2n","n2w"]; 35 36AddBinop ("ADD32", (``UNCURRY $+ : word32#word32->word32``, "+")); 37AddBinop ("SUB32", (``UNCURRY $- : word32#word32->word32``, "-")); 38AddBinop ("LESS32", (``UNCURRY $< : word32#word32->bool``, "<")); 39AddBinop ("EQ32", (``UNCURRY $= : word32#word32->bool``, "==")); 40 41(*****************************************************************************) 42(* 32-bit MUX *) 43(*****************************************************************************) 44 45add_vsynth 46 [(``\(sel:bool,in1:word32,in2:word32). if sel then in1 else in2``, 47 fn [i1,i2,i3] => (i1 ^ " ? " ^ i2 ^ " : " ^ i3)) 48 ]; 49 50(*****************************************************************************) 51(* We implement multiplication with a naive iterative multiplier function *) 52(* (works by repeated addition) *) 53(*****************************************************************************) 54 55val (Mult32Iter,Mult32Iter_ind,Mult32Iter_cir) = 56 compile.cirDefine 57 `(Mult32Iter (m:word32,n:word32,acc:word32) = 58 if m = 0w then (0w:word32,n,acc) 59 else Mult32Iter(m-1w,n,n + acc)) 60 measuring (w2n o FST)`; 61 62(*****************************************************************************) 63(* Create an implementation of a multiplier from Mult32Iter *) 64(*****************************************************************************) 65 66val (Mult32,_,Mult32_cir) = 67 compile.cirDefine 68 `Mult32(m,n) = SND(SND(Mult32Iter(m,n,0w)))`; 69 70(*****************************************************************************) 71(* Implement iterative function as a step to implementing factorial *) 72(*****************************************************************************) 73 74val (Fact32Iter,Fact32Iter_ind,Fact32Iter_cir) = 75 compile.cirDefine 76 `(Fact32Iter (n:word32,acc:word32) = 77 if n = 0w then (n,acc) 78 else Fact32Iter(n-1w, Mult32(n,acc))) 79 measuring (w2n o FST)`; 80 81(*****************************************************************************) 82(* Implement a function Fact32 to compute SND(Fact32Iter (n,1)) *) 83(*****************************************************************************) 84 85val (Fact32,_,Fact32_cir) = 86 compile.cirDefine 87 `Fact32 n = SND(Fact32Iter (n,1w))`; 88 89(*****************************************************************************) 90(* This dumps changes to all variables. Set to false to dump just the *) 91(* changes to module Fact32. *) 92(*****************************************************************************) 93 94dump_all_flag := true; 95 96(*****************************************************************************) 97(* Change these variables to select simulator and viewer. Commenting out the *) 98(* three assignments below will revert to the defaults: cver/dinotrace. *) 99(*****************************************************************************) 100 101iverilog_path := "/usr/bin/iverilog"; 102verilog_simulator := iverilog; 103waveform_viewer := gtkwave; 104 105(*****************************************************************************) 106(* Stop zillions of warning messages that HOL variables of type ``:num`` *) 107(* are being converted to Verilog wires or registers of type [31:0]. *) 108(*****************************************************************************) 109 110numWarning := true; 111 112SIMULATE Fact32_cir [("inp","4")]; 113 114val _ = export_theory(); 115