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