-
Notifications
You must be signed in to change notification settings - Fork 140
/
README
846 lines (613 loc) · 29.7 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
===============================================================================
== This directory contains Juliano's HOL files modified by MJCG & KXS ==
== [see end of this file for version history] ==
===============================================================================
composeScript.sml ......... definition of devices and their composition
devScript.sml.............. definition and theorems on liveness
compileScript.sml ......... definitions and theorems to support compiler
compile.sml ............... convert to combinators and compile to circuits
vsynth.sml ................ convert a circuit made with MAKE_CIRCUIT to Verilog
FactScript.sml ............ synthesise naive factorial and dump Verilog
Fact.ml ................... synthesise and simulate factorial and run gtkwave
Fact32 .................... directory with word32 examples (including factorial)
dff ....................... Melham's temporal abstraction theory
Holmakefile ............... instructions for Holmake
*******************************************************************************
There are six levels of abstraction:
S: Source (subset of TFL)
I: Intermediate (source combinators Atm, Seq, Par, Ite, Rec)
D: Devices (handshake hardware combinators: ATM, SEQ, PAR, ITE, REC)
N: Netlist (abstract device predicates: unclocked DEL, DELT, DELT and DFF)
C: Circuit (clocked synchronous device predicates: Dtype, Dff)
V: Verilog (netlist pretty-printed into Verilog)
The main user-level functions are hwDefine, cirDefine, REFINE_ALL and
MAKE_NETLIST for creating hardware, refining it and then creating a
netlist representation, and MAKE_CIRCUIT and MAKE_VERILOG for creating
Verilog HDL output.
*******************************************************************************
To make generated hardware devices a bit more readable, the following
(experimental) infixes are now defined in composeScript.sml
set_fixity ";;" (Infixl 750); overload_on (";;", ``SEQ``)
set_fixity "||" (Infixl 650); overload_on ("||", ``PAR``)
The bus concatenation operator <> is defined by:
|- !f g. f <> g = (\t. (f t,g t))
Abstract device netlists are generated by MAKE_NETLIST and contain the
following combinational components:
|- COMB f (inp,out) = !t. out t = f (inp t)
|- CONSTANT c out = !t. out t = c
|- MUX (sel,in1,in2,out) = !t. out t = (if sel t then in1 t else in2 t
|- AND (in1,in2,out) = !t. out t = in1 t /\ in2 t
|- OR (in1,in2,out) = !t. out t = in1 t \/ in2 t
|- NOT (inp,out) = !t. out t = ~inp t
and sequential components (registers):
|- DEL (inp,out) = !t. out(t+1) = inp t
|- DELT(inp,out) = (out 0 = T) /\ !t. out(t+1) = inp t
|- DELF(inp,out) = (out 0 = F) /\ !t. out(t+1) = inp t
|- DFF (d,clk,q) = !t. q(t+1) = if POSEDGE clk (t+1) then d(t+1) else q t
where:
|- POSEDGE s t = if t=0 then F else ~s(t-1) /\ s t
The sequential components are then implemented in terms of clocked reqisters:
|- Dtype (ck,d,q) = !t. q (t+1) = (if Rise ck t then d t else q t)
|- DtypeT (ck,d,q) = (q 0 = T) /\ Dtype(ck,d,q)
|- DtypeF (ck,d,q) = (q 0 = F) /\ Dtype(ck,d,q)
where:
|- Rise s t = ~(s t) /\ s(t+1)
The implementation of DEL, DELT, DELF, DFF in terms of Dtype, DtypeT
and DtypeF involves a temporal abstraction, since Dtype and the
flip-flops are edge-triggered on a clock, but DEL, DELT, DELF, DFF are
not. The refinement from the unclocked level of abstraction to the
clocked circuit level is implemented formally using infrastructure
from Melham's theory of temporal abstraction in the directory dff:
Using Melham's dff theories it is proved in compileScript.sml that:
|- InfRise clk ==> !d q. Dtype (clk,d,q) ==> DEL (d at clk,q at clk)
|- InfRise clk ==> !d q. DtypeT (clk,d,q) ==> DELT (d at clk,q at clk)
|- InfRise clk ==> !d q. DtypeF (clk,d,q) ==> DELF (d at clk,q at clk)
Where
|- Inf sig = !t. ?t'. t < t' /\ sig t' (* sig true infinitely often) *)
|- InfRise clk = Inf(Rise clk) (* clk has infinitely many rising edges *)
|- s at clk = s when (Rise clk) (* s sampled at rising edges of clk *)
The term ``(s when P) n`` gives the value of s at the time when P is
true on the n-th occasion (``when`` is defined using the choice
operator in dff/tempabsScript.sml). Thus ``s at clk`` is ``s`` sampled
at rising edges of ``clk`` (the sampling being just before the clock rises).
Note that ``s at clk`` is similar to ``s@clk`` in PSL.
Clocked synchronous circuits using combinational logic and the
registers Dtype and Dff are synthesised using MAKE_CIRCUIT.
*******************************************************************************
hwDefine : term frag list -> thm * thm * thm
--------------------------------------------
Single entrypoint for definitions where proof of termination will
succeed. Allows measure function to be indicated in same quotation as
definition, or not.
hwDefine lib `(eqns) measuring f`
will use f as the measure function and attempt automatic termination
proof. If successful, returns (|- eqns, |- ind, |- dev)
NB. the recursion equations must be parenthesized; otherwise, strange
parse errors result. Also, the name of the defined function must be
alphanumeric.
One can also not mention the measure function, as in Define:
hwDefine `eqns`
which will accept either non-recursive or recursive specifications. It
returns a triple (|- eqns, |- ind, |- dev) where the ind theorem
should be ignored (it will be boolTheory.TRUTH).
The result of a call to hwRefine is added to the front of a global
reference hwDefineLib, which is accessed by REFINE_ALL.
See FactScript.sml for examples.
REFINE: (term -> thm) -> thm -> thm
-----------------------------------
The first argument of REFINE is a "refine function", refine say,
which maps a term representing a circuit, <circuit> say, to a theorem
|- <circuit'> ===> <circuit>
where ``===>`` is defined by:
|- P ===> Q = !x. P x ==> Q x.
and <circuit'> is a term representing the result of refining <circuit>
with the function refine.
Evaluating
REFINE refine (|- <circuit> ===> Dev f)
applies refine to <circuit> to get
|- <circuit'> ===> <circuit>
and then uses transitivity of ===> (DEV_IMP_TRANS) to deduce:
|- <circuit'> ===> Dev f
Two useful refine functions are ATM_REFINE and LIB_REFINE.
ATM_REFINE : term -> thm
------------------------
This maps ``DEV f`` to |- ATM f ===> DEV f
LIB_REFINE : thm list -> term -> thm
------------------------------------
Evaluating
LIB_REFINE
[|- <circuit> ===> DEV f1,
|- <circuit> ===> DEV f2
...
|- <circuit> ===> DEV fn]
``DEV fi``
returns the first theorem |- <circuit> ===> DEV fi that it finds in
the supplied list (i.e. the supplied library). Fails if no refinement
theorem found.
Refinement functions (analogously to conversions and tactics) can be
combined using combinators THENR, ORELSER, REPEATR, DEPTHR.
THENR : (term -> thm) * (term -> thm) -> (term -> thm)
------------------------------------------------------
Combines refinements sequentially.
ORELSER : (term -> thm) * (term -> thm) -> (term -> thm)
--------------------------------------------------------
Tries first refinement and if that fails tries the second one.
REPEATR : (term -> thm) -> term -> thm
--------------------------------------
Repeates a refinement until no change. Will fail if the refinement
being repeated fails.
ALL_REFINE: term -> thm
-----------------------
ALL_REFINE tm evaluatges to the identity refinement |- tm ===> tm
DEPTHR : (term -> thm) -> (term -> thm)
---------------------------------------------
Scans through a term representing a circuit applying the supplied
refinement function to each subterm of the form ``DEV f`` and
either generating
|- DEV g ===> DEV f
if the refinement function returns this, or, if the refinement
function fails:
|- DEV f ===> DEV f
A refined circuit is then build up using the "monotonicity" theorems:
SEQ_DEV_IMP =
|- !P1 P2 Q1 Q2.
P1 ===> Q1 /\ P2 ===> Q2
==>
(SEQ P1 P2 ===> SEQ Q1 Q2)
PAR_DEV_IMP =
|- !P1 P2 Q1 Q2.
P1 ===> Q1 /\ P2 ===> Q2
==>
(PAR P1 P2 ===> PAR Q1 Q2)
ITE_DEV_IMP =
|- !P1 P2 P3 Q1 Q2 Q3.
P1 ===> Q1 /\ P2 ===> Q2 /\ P3 ===> Q3
==>
(ITE P1 P2 P3 ===> ITE Q1 Q2 Q3)
REC_DEV_IMP =
|- !P1 P2 P3 Q1 Q2 Q3.
P1 ===> Q1 /\ P2 ===> Q2 /\ P3 ===> Q3
==>
(REC P1 P2 P3 ===> REC Q1 Q2 Q3)
PRECEDE_DEV_IMP
|- !f P Q. P ===> Q ==> PRECEDE f P ===> PRECEDE f Q
Note that "DEPTHR refine" should never fail.
REFINE: thm -> thm
------------------
Refine using definitions in hwDefineLib and then convert all remaining
DEVs to ATMs. The definition is:
fun REFINE_ALL th =
REFINE
(REPEATR
(DEPTHR
(LIB_REFINE(map #3 (!hwDefineLib))
ORELSER ATM_REFINE
ORELSER ALL_REFINE)))
th;
add_combinational : string list -> unit
---------------------------------------
Add a list of constant names to the constants that are implemented as
combinational by the compiler. The definition is:
fun add_combinational l =
(combinational_constants := union l (!combinational_constants));
The initial list of combinational constant names (i.e. the initial
value of the reference combinational_constants) is:
["T","F","/\\","\\/","~",",","o","CURRY","UNCURRY","COND",
"FST","SND","=","Seq","Par","Ite","0","NUMERAL","BIT1","BIT2","ZERO",
"+","-"];
is_combinational : term -> bool
-------------------------------
Test whether a terms is a combinational function of its free variables
(i.e. is built up using only combinational constants).
AddUnop : string * (term * string) -> unit
------------------------------------------
Evaluating
AddUnop("<component name>", (``<HOL operator>``, "<Verilog operator>"))
defines a HOL component and a corresponding Verilog module and adds
these to the synthesis engine. Currently only types ``:bool``,
``:num`` and ``:word<n>`` are supported; ``:num`` is converted to
Verilog words of width [31:0] (and a warning is issued, since this is
in general invalid). Example:
AddUnop ("NOT32", (``$~:word32->word32`` , "~"));
If one doesn't intend to generate Verilog, then just give an arbitrary
string as the Verilog operator (invoking PRINT_VERILOG will then print
a module that uses this string, but you will only get an error when
the Verilog is used, e.g. a simulation is attempted).
AddBinop : string * (term * string) -> unit
-------------------------------------------
Evaluating
AddBinop
("<component name>",
(``<uncurried HOL binary operator>``, "<Verilog operator>"))
defines a HOL component and a corresponding Verilog module and adds
these to the synthesis engine. Currently only types ``:bool``,
``:num`` and ``:word<n>`` are supported; ``:num`` is converted to
Verilog words of width [31:0] (and a warning is issued, since this is
in general invalid). Examples:
AddBinop ("ADD", (``UNCURRY $+ : num#num->num``, "+"))
AddBinop ("SUB", (``UNCURRY $- : num#num->num``, "-"))
AddBinop ("ADD32", (``UNCURRY $+ : word32#word32->word32``, "+"));
AddBinop ("SUB32", (``UNCURRY $- : word32#word32->word32``, "-"))
AddBinop ("LESS32", (``UNCURRY $< : word32#word32->bool``, "<"));
AddBinop ("EQ32", (``UNCURRY $= : word32#word32->bool``, "=="))
If one doesn't intend to generate Verilog, then just give an arbitrary
string as the Verilog operator (invoking PRINT_VERILOG will then print
a module that uses this string, but you will only get an error when
the Verilog is used, e.g. a simulation is attempted).
MAKE_NETLIST : thm -> thm
-------------------------
Evaluating
MAKE_NETLIST (|- <device> ===> DEV f)
unfolds <device> using the definitions of ATM, SEQ, PAR, ITE and REC
and normalises the resulting term into a form, <netlist> say,
corresponding to a netlist, and returns
|- <netlist>
==>
DEV f (load,(inp1<>...<>inpm),done,(out1<>...<>outn))
MAKE_CIRCUIT : thm -> thm
-------------------------
Evaluating
MAKE_CIRCUIT (|- <device> ===> DEV f)
unfolds <device> into a netlist, then replaces DFF by an
implementation in terms of DEL and DELT, and then, using Melham's
temporal abstraction theory in dff, refines any unclocked DEL, DELT
and DELF to clocked Dtype and Dff, and returns:
|- InfClock clk
==>
<circuit>
==>
DEV f (load at clk,
(inp1<>...<>inpm) at clk,
done at clk,
(out1<>...<>outn) at clk)
See FactScript.sml for examples (e.g. FACT_cir).
cirDefine : term frag list -> thm * thm * thm
--------------------------------------------
Invoke hwDefine and then apply MAKE_CIRCUIT and REFINE_ALL to the device:
fun cirDefine qdef =
let val (def,ind,dev) = hwDefine qdef
in
(def, ind, MAKE_CIRCUIT(REFINE_ALL dev))
end;
PRINT_VERILOG : thm -> unit
---------------------------
Evaluating
PRINT_VERILOG
(|- InRise clk
==>
(?v0 .... vn. <circuit>)
==>
DEV fun (load at clk,
(inp1 <> ... <> inpu) at clk,
done at clk,
(out1 <> ... <> outv) at clk))
creates a module called fun that has the definitions of the modules
used in <circuit>, and prints it and the definitions it needs to
fun.vl.
The header is:
module fun (clk,load,inp1,...,inpu,done,out1,...,outv);
input clk,load;
input [<size>:0] inp1,inp2;
output done;
output [<size>:0] out;
wire clk,done;
where <size> is the appropriate width computed from the types. The
internal variables v0, ... ,vn are declared to be wires of appropriate
widths (computed from their types).
Types ``:num`` are converted to Verilog wires or registers of width
[31:0], which is not in general valid. When such a conversion occurs,
a warning like:
Warning: type of inp is ``:num``, but is compiled to [31:0].
is printed. These warnings can be suppressed by evaluating:
numWarning := false;
(the ML reference numWarning has a default of true).
SIMULATE : thm -> (string * string) list -> unit
------------------------------------------------
If thm is:
|- InRise clk
==>
(?v0 .... vn. <circuit>)
==>
DEV fun (load at clk,
(inp1 <> ... <> inpu) at clk,
done at clk,
(out1 <> ... <> outv) at clk)
the evaluating:
SIMULATE thm [("inp1","val1"),...,("inpn","valn")]
dumps Verilog using
PRINT_SIMULATION thm (!period_default) [("inp1","val1"),...,("inpn","valn")]
(see below). It then runs a Verilog simulator on fun.vl and then calls
a waveform viewer on fun.vcd.
Currently iverilog (Icarus Verilog:
http://www.icarus.com/eda/verilog/) and cver (GPL Cver:
http://www.pragmatic-c.com/gpl-cver/) are supported as Verilog
simulators and gtkwave (GTKWave:
ftp://ftp.cs.man.ac.uk/pub/amulet/balsa/other-software/gtkwave-2.0.0pre5.tar.gz)
and dinotrace (which comes with GPS Cver) as waveform viewers.
GPS Cver and dinotrace are particularly easy to install, and are now
the default. To install them, connect to examples/dev and execute:
wget http://www.pragmatic-c.com/gpl-cver/downloads/gplcver-2.10c.linux.bin.tar.bz2;
bunzip2 gplcver-2.10c.linux.bin.tar.bz2;
tar -xf gplcver-2.10c.linux.bin.tar
which should create a directory gplcver-2.10c.linux.bin.
SIMULATE should then just work. Test by evaluating "use Fact.ml;" in hol,
which should launch dinotrace showing a trace of FACT 4 being computed.
You can change the default clock period, which is held in a reference
val period_default = ref 5;
To change the default simulator and viewer change the references
verilog_simulator and waveform_viewer. For example, to change to
iverilog and gtkwave do:
val verilog_simulator = ref iverilog;
val waveform_viewer = ref gtkwave;
The executables are held in references, which have default values:
val iverilog_path = ref "/usr/bin/iverilog";
val vvp_path = ref "/usr/bin/vvp";
val gtkwave_path = ref "/usr/bin/gtkwave -a";
val cver_path = ref "./gplcver-2.10c.linux.bin/bin/cver";
val dinotrace_path = ref "./gplcver-2.10c.linux.bin/bin/dinotrace";
Note that cver_path and dinotrace_path are correct if the installation
described above is performed.
PRINT_SIMULATION : thm -> int -> (string * string) list -> unit
---------------------------------------------------------------
Evaluating
PRINT_SIMULATION thm period stimulus
prints both the Verilog corresponding to thm (see PRINT_VERILOG) and
then adds a clock and a module Main containing an instance of the
clock and an instance of the module generated from thm.
The instance of Clock is created with time between edges as specified
by the parameter period (so really period is 2*period).
The clock line clk and the handshake completion line done are declared
to be boolean wires.
The input load is declared to be a boolean register and the inputs
inp1, ... ,inpu are declared to be registers of the appropriate width.
A dumpfile called "file.vcd" is created. If the reference variable
dump_all_flag is false (the default) then only changes to clk, load,
and signals inp1, ... ,inpu, done, out1, ... ,outv are declared to
have their changes dumped to the VCD file. If dump_all_flag is true,
then changes to all variables are dumped.
The input variables are driven according to the parameter stimulus,
which is an ML list of tuples of the form:
[("inp1",val),...,("inpu",val)]
where each input is driven with the supplied value (a string that
prints to a valid Verilog expression).
I am using Icarus Verilog for simulation
(http://www.icarus.com/eda/verilog/) and GTKWave
(http://www.cs.man.ac.uk/apt/tools/gtkwave/) for viewing VCD files.
Both are public domain and seem to work.
*******************************************************************************
Auxiliary functions of interest include the following.
Convert : thm -> thm
--------------------
Convert (|- f x = e) returns a theorem |- f = p, where p is a
combinatory expression built from the combinators Seq, Par and Ite.
RecConvert: : thm -> thm -> thm
-------------------------------
RecConvert (|- f x = if f1 x then f2 x else f(f3 x)) (|- TOTAL(f1,f2,f3))
returns a theorem
|- f = Rec(p1,p2,p3)
where p1, p2 and p3 are combinatory expressions built from the
combinators Seq, Par and Ite.
A term PRECEDE f d represents a device d preceded by combinational
logic and a term FOLLOW d f represents a device d followed by
combinational logic.
|- PRECEDE f d =
(\(load,inp,done,out). ?v. COMB f (inp,v) /\ d(load,v,done,out))
|- FOLLOW d f =
(\(load,inp,done,out). ?v. d(load,inp,done,v) /\ COMB f (v,out))
The function f representing the combinational logic must only contain
constants declared combinational by having their names included in the
ML assignable list "combinational_constants".
Currently PRECEDE and FOLLOW are eliminated when generating netlists,
but they may appear in the output of the compiler (see the
CompileConvert example below).
CompileProg : thm list -> term -> thm
-------------------------------------
CompileProg takes a program and a constant defined in the program
CompileProg : thm list -> term -> thm
-------- ----
program constant
When the compiler encounters a function f that isn't an application of
Seq, Par or Ite, then DEV f is generated. It is assumed this
will subsequently be refined to hardware (see Refine).
Compile : thm -> thm
--------------------
Compile (|- c = e) = CompileProg [|- c = e] ``c``
CompileConvert : thm -> thm
---------------------------
Converts a non-recursive equation to combinators and then compiles to
a device implementation.
Example:
Fact;
> val it = |- !n. Fact n = SND (FactIter (n,1)) : thm
- CompileConvert Fact;
> val it =
|- FOLLOW (PRECEDE (Par (\n. n) (\n. 1)) (DEV FactIter)) SND
===>
DEV Fact : thm
RecCompileConvert : thm -> thm -> thm
-------------------------------------
Converts a recursive equation to combinators and then compiles to a
device implementation. Needs a totality theorem (user-supplied as third
argument).
Example:
- val FactIter =
|- FactIter (n,acc) =
(if n = 0 then (n,acc) else FactIter (n - 1,n * acc))
- val FactIter_TOTAL =
|- TOTAL
((\(n,acc). n = 0),(\(n,acc). (n,acc)),(\(n,acc). (n - 1,n * acc)))
- RecCompileConvert FactIter FactIter_TOTAL;
> val it =
|- REC(FOLLOW (DEV (\(n,acc). n) || DEV (\(n,acc). 0)) (UNCURRY $=))
(DEV (\x. x))
(DEV (\x. FST x - 1) || PRECEDE (\x. x) (DEV (UNCURRY $*)))
===>
DEV FactIter
COMB_SYNTH_CONV : term -> thm
-----------------------------
One step of conversion of
``COMB
(\(i1,...,im). (<term1>,...,<termn>)
(inp1 <> ... <> inpm, out1 <> .... outn)``
to a netlist.
Example:
- COMB_SYNTH_CONV
``COMB (\(m,n,p). (m-p, SUC(m+n+(p-1)))) (in1<>in2<>in3,out1<>out2)``;
> val it =
|- COMB (\(m,n,p). (m - p,SUC (m + n + (p - 1))))
(in1 <> in2 <> in3,out1 <> out2) =
COMB (\(m,n,p). m - p) (in1 <> in2 <> in3,out1) /\
COMB (\(m,n,p). SUC (m + n + (p - 1))) (in1 <> in2 <> in3,out2) : thm
To completely convert to a netlist COMB_SYNTH_CONV needs to be
iterated. Example:
- REDEPTH_CONV COMB_SYNTH_CONV
``COMB (\(m,n,p). (m-p, SUC(m+n+(p-1)))) (in1<>in2<>in3,out1<>out2)``;
> val it =
|- COMB (\(m,n,p). (m - p,SUC (m + n + (p - 1))))
(in1 <> in2 <> in3,out1 <> out2) =
(?v709 v710.
(v709 = in1) /\ (v710 = in3) /\
COMB (UNCURRY $-) (v709 <> v710,out1)) /\
?v711.
(?v712 v713.
(?v714 v715.
(v714 = in1) /\ (v715 = in2) /\
COMB (UNCURRY $+)
(v714 <> v715,v712)) /\
(?v716 v717.
(v716 = in3) /\ CONSTANT 1 v717 /\
COMB (UNCURRY $-)
(v716 <> v717,v713)) /\
COMB (UNCURRY $+)
(v712 <> v713,v711)) /\
COMB SUC (v711,out2) : thm
Note that the redundant variables are pruned by MAKE_NETLIST and also,
for readability, the example above uses ``v709`` but COMB_SYNTH_CONV
actually generates ``%%genvar%%709`.
COMB_SYNTH_CONV may print out some diagnostic stuff if it fails to
prove certain subgoals (though it may nevertheless still produce
something reasonable). This output can be switched off by setting the
ML reference "if_print_flag" to false.
===============================================================================
====== ML definitions and commands to define 32-bit bitwise exclusive-or ======
===============================================================================
(*****************************************************************************)
(* The sources have lots of cut-and-paste-and-tweak style repetition for the *)
(* various combinational components (NOT, AND, OR, MUX, ADD, SUB, LESS, EQ). *)
(* *)
(* The functions AddUnop and AddBinop cope with some of the repetition, *)
(* but what follows might also be useful documentation. *)
(* *)
(* Here are the steps currently needed to add a new component, *)
(* illustrated with the addition of 32-bit bitwise exclusive-or (XOR32). *)
(* *)
(* These steps are a manual version of what is done when *)
(* *)
(* AddBinop ("XOR32", (``UNCURRY $# : word32#word32->word32``, "^")); *)
(* *)
(* is evaluated. *)
(*****************************************************************************)
(*****************************************************************************)
(* Step 1 *)
(* ------ *)
(* Define the component in HOL *)
(* (assumes word32Theory loaded and open) *)
(*****************************************************************************)
val XOR32_def =
Define
`XOR32(in1,in2,out) = !t. out t = (in1 t) # (in2 t)`;
(*****************************************************************************)
(* Step 2 *)
(* ------ *)
(* Prove some boilerplate theorems and add to global lists: *)
(*****************************************************************************)
val COMB_XOR32 =
store_thm
("COMB_XOR32",
``COMB (UNCURRY $#) (in1 <> in2, out) = XOR32(in1,in2,out)``,
RW_TAC std_ss [COMB_def,BUS_CONCAT_def,XOR32_def]);
add_combinational_components[COMB_XOR32];
val XOR32_at =
store_thm
("XOR32_at",
``XOR32(in1,in2,out)
==>
XOR32(in1 at clk,in2 at clk,out at clk)``,
RW_TAC std_ss [XOR32_def,at_def,tempabsTheory.when]);
add_temporal_abstractions[XOR32_at];
(*****************************************************************************)
(* Step 3 *)
(* ------ *)
(* Define a Verilog module as an ML string (XOR32vDef), a function to *)
(* create an instance with a given size as a string (XOR32vInst), an *)
(* instance counter (XOR32vInst_count -- used to create unique names for *)
(* instances) and a function to print a HOL term ``XOR32(in1,in2,out)`` as *)
(* an instance, using the the type of ``out`` to compute the word width *)
(* needed to set parameter "size" in XOR32vDef (termToVerilog_XOR32). *)
(* These functions are added to a couple of global lists. *)
(*****************************************************************************)
val XOR32vDef =
"// Combinational bitwise XOR32\n\
\module XOR32 (in1,in2,out);\n\
\ parameter size = 31;\n\
\ input [size:0] in1,in2;\n\
\ output [size:0] out;\n\
\\n\
\ assign out = in1 ^ in2;\n\
\\n\
\endmodule\n\
\\n";
val XOR32vInst_count = ref 0;
fun XOR32vInst (out:string->unit) [("size",size)] [in1_name,in2_name,out_name] =
let val count = !XOR32vInst_count
val _ = (XOR32vInst_count := count+1);
val inst_name = "XOR32" ^ "_" ^ Int.toString count
in
(out " XOR32 "; out inst_name;
out " (";out in1_name;out",";out in2_name;out",";out out_name; out ");\n";
out " defparam ";out inst_name; out ".size = "; out size;
out ";\n\n")
end;
add_module ("XOR32", (XOR32vDef, XOR32vInst));
fun termToVerilog_XOR32 (out:string->unit) tm =
if is_comb tm
andalso is_const(fst(strip_comb tm))
andalso (fst(dest_const(fst(strip_comb tm))) = "XOR32")
andalso is_pair(rand tm)
andalso (length(strip_pair(rand tm)) = 3)
andalso all is_var (strip_pair(rand tm))
then XOR32vInst
out
[("size", var2size(last(strip_pair(rand tm))))]
(map (fst o dest_var) (strip_pair(rand tm)))
else raise ERR "termToVerilog_XOR32" "bad component term";
termToVerilogLib := (!termToVerilogLib) @ [termToVerilog_XOR32];
===============================================================================
== This directory contains Juliano's HOL files modified by MJCG & KXS ==
== [Revised version incorporating Juliano's new treatment of recursion] ==
== [Revised version incorporating liveness] ==
== [04.01.05: improved proofs from KXS in composeScript.sml & devScript.sml] ==
== [09.01.05: MJCG added converter to combinators Seq, Par, Ite, Rec] ==
== [13.01.05: major tidy and update by MJCG] ==
== [17.01.05: MJCG installed hwDefine and improved examples from KXS] ==
== [18.01.05: MJCG added Refine and revised FactScript.sml] ==
== [19.01.05: MJCG changed to use refinement combinators] ==
== [20.01.05: MJCG added netlist synthesis] ==
== [21.01.05: MJCG minor changes and README update] ==
== [27.01.05: MJCG added hw synthesis improvements] ==
== [28.01.05: MJCG more optimisations and updated README] ==
== [29.01.05: MJCG added COMB_SYNTH_CONV removed SEL operators] ==
== [30.01.05: MJCG added dff: Melham's temporal abstraction theory] ==
== [01.02.05: MJCG minor tweaks to MAKE_NETLIST and COMB_SYNTH_CONV] ==
== [06.02.05: MJCG added refinement to clocked dtype registers] ==
== [08.02.05: MJCG added ?-quantification of internal wires to MAKE_CIRCUIT] ==
== [10.02.05: MJCG split input and output busses] ==
== [11.02.05: Holmakefile (thanks to MN) + code improvements (thanks to KXS)]==
== [14.02.05: MJCG added vsynth (defines MAKE_VERILOG)] ==
== [15.02.05: MJCG revised MAKE_NETLIST and MAKE_CIRCUIT] ==
== [18.02.05: MJCG revised MAKE_VERILOG in vsynth; added MAKE_SIMULATION] ==
== [28.02.05: MJCG revised added SIMULATE to run iverilog and gtkwave] ==
== [20.04.05: MJCG updated section on adding new components] ==
== [17.05.05: MJCG added hwDefineLib and REFINE_ALL] ==
== [30.05.05: MJCG added cirDefine] ==
===============================================================================