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
|
<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" />
<title>HTLBlockgen.v</title>
<link rel="stylesheet" href="alectryon.css" type="text/css" />
<link rel="stylesheet" href="docutils_basic.css" type="text/css" />
<link rel="stylesheet" href="tango_subtle.css" type="text/css" />
<link rel="stylesheet" href="tango_subtle.min.css" type="text/css" />
<script type="text/javascript" src="alectryon.js"></script>
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" />
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" />
</head>
<body>
<div class="alectryon-root alectryon-floating"><div class="document">
<pre class="alectryon-io"><!-- Generator: Alectryon v1.0 --><span class="coq-wsp"><span class="highlight"><span class="c">(* </span>
<span class="c"> * Vericert: Verified high-level synthesis.</span>
<span class="c"> * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com></span>
<span class="c"> *</span>
<span class="c"> * This program is free software: you can redistribute it and/or modify</span>
<span class="c"> * it under the terms of the GNU General Public License as published by</span>
<span class="c"> * the Free Software Foundation, either version 3 of the License, or</span>
<span class="c"> * (at your option) any later version.</span>
<span class="c"> *</span>
<span class="c"> * This program is distributed in the hope that it will be useful,</span>
<span class="c"> * but WITHOUT ANY WARRANTY; without even the implied warranty of</span>
<span class="c"> * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the</span>
<span class="c"> * GNU General Public License for more details.</span>
<span class="c"> *</span>
<span class="c"> * You should have received a copy of the GNU General Public License</span>
<span class="c"> * along with this program. If not, see <https://www.gnu.org/licenses/>.</span>
<span class="c"> *)</span>
<span class="c">(*From compcert Require Import Maps.</span>
<span class="c">From compcert Require Errors Globalenvs Integers.</span>
<span class="c">From compcert Require Import AST.</span>
<span class="c">From vericert Require Import RTLBlock Verilog HTL Vericertlib AssocMap ValueInt Statemonad.</span>
<span class="c">Hint Resolve AssocMap.gempty : htlh.</span>
<span class="c">Hint Resolve AssocMap.gso : htlh.</span>
<span class="c">Hint Resolve AssocMap.gss : htlh.</span>
<span class="c">Hint Resolve Ple_refl : htlh.</span>
<span class="c">Hint Resolve Ple_succ : htlh.</span>
<span class="c">Record state: Type := mkstate {</span>
<span class="c"> st_st : reg;</span>
<span class="c"> st_freshreg: reg;</span>
<span class="c"> st_freshstate: node;</span>
<span class="c"> st_scldecls: AssocMap.t (option io * scl_decl);</span>
<span class="c"> st_arrdecls: AssocMap.t (option io * arr_decl);</span>
<span class="c"> st_datapath: datapath;</span>
<span class="c"> st_controllogic: controllogic;</span>
<span class="c">}.</span>
<span class="c">Definition init_state (st : reg) : state :=</span>
<span class="c"> mkstate st</span>
<span class="c"> 1%positive</span>
<span class="c"> 1%positive</span>
<span class="c"> (AssocMap.empty (option io * scl_decl))</span>
<span class="c"> (AssocMap.empty (option io * arr_decl))</span>
<span class="c"> (AssocMap.empty stmnt)</span>
<span class="c"> (AssocMap.empty stmnt).</span>
<span class="c">Module HTLState <: State.</span>
<span class="c"> Definition st := state.</span>
<span class="c"> Inductive st_incr: state -> state -> Prop :=</span>
<span class="c"> state_incr_intro:</span>
<span class="c"> forall (s1 s2: state),</span>
<span class="c"> st_st s1 = st_st s2 -></span>
<span class="c"> Ple s1.(st_freshreg) s2.(st_freshreg) -></span>
<span class="c"> Ple s1.(st_freshstate) s2.(st_freshstate) -></span>
<span class="c"> (forall n,</span>
<span class="c"> s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -></span>
<span class="c"> (forall n,</span>
<span class="c"> s1.(st_controllogic)!n = None</span>
<span class="c"> \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -></span>
<span class="c"> st_incr s1 s2.</span>
<span class="c"> Hint Constructors st_incr : htlh.</span>
<span class="c"> Definition st_prop := st_incr.</span>
<span class="c"> Hint Unfold st_prop : htlh.</span>
<span class="c"> Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed.</span>
<span class="c"> Lemma st_trans :</span>
<span class="c"> forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3.</span>
<span class="c"> Proof.</span>
<span class="c"> intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence.</span>
<span class="c"> - destruct H4 with n; destruct H8 with n; intuition congruence.</span>
<span class="c"> - destruct H5 with n; destruct H9 with n; intuition congruence.</span>
<span class="c"> Qed.</span>
<span class="c">End HTLState.</span>
<span class="c">Export HTLState.</span>
<span class="c">Module HTLMonad := Statemonad(HTLState).</span>
<span class="c">Export HTLMonad.</span>
<span class="c">Module HTLMonadExtra := Monad.MonadExtra(HTLMonad).</span>
<span class="c">Import HTLMonadExtra.</span>
<span class="c">Export MonadNotation.</span>
<span class="c">Definition state_goto (st : reg) (n : node) : stmnt :=</span>
<span class="c"> Vnonblock (Vvar st) (Vlit (posToValue n)).</span>
<span class="c">Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt :=</span>
<span class="c"> Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)).</span>
<span class="c">Definition check_empty_node_datapath:</span>
<span class="c"> forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }.</span>
<span class="c">Proof.</span>
<span class="c"> intros. case (s.(st_datapath)!n); tauto.</span>
<span class="c">Defined.</span>
<span class="c">Definition check_empty_node_controllogic:</span>
<span class="c"> forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }.</span>
<span class="c">Proof.</span>
<span class="c"> intros. case (s.(st_controllogic)!n); tauto.</span>
<span class="c">Defined.</span>
<span class="c">Lemma add_instr_state_incr :</span>
<span class="c"> forall s n n' st,</span>
<span class="c"> (st_datapath s)!n = None -></span>
<span class="c"> (st_controllogic s)!n = None -></span>
<span class="c"> st_incr s</span>
<span class="c"> (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> s.(st_freshreg)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> (AssocMap.set n st s.(st_datapath))</span>
<span class="c"> (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))).</span>
<span class="c">Proof.</span>
<span class="c"> constructor; intros;</span>
<span class="c"> try (simpl; destruct (peq n n0); subst);</span>
<span class="c"> auto with htlh.</span>
<span class="c">Qed.</span>
<span class="c">Lemma declare_reg_state_incr :</span>
<span class="c"> forall i s r sz,</span>
<span class="c"> st_incr s</span>
<span class="c"> (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> s.(st_freshreg)</span>
<span class="c"> s.(st_freshstate)</span>
<span class="c"> (AssocMap.set r (i, VScalar sz) s.(st_scldecls))</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> s.(st_datapath)</span>
<span class="c"> s.(st_controllogic)).</span>
<span class="c">Proof. auto with htlh. Qed.</span>
<span class="c">Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=</span>
<span class="c"> fun s => OK tt (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> s.(st_freshreg)</span>
<span class="c"> s.(st_freshstate)</span>
<span class="c"> (AssocMap.set r (i, VScalar sz) s.(st_scldecls))</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> s.(st_datapath)</span>
<span class="c"> s.(st_controllogic))</span>
<span class="c"> (declare_reg_state_incr i s r sz).</span>
<span class="c">Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit :=</span>
<span class="c"> fun s =></span>
<span class="c"> match check_empty_node_datapath s n, check_empty_node_controllogic s n with</span>
<span class="c"> | left STM, left TRANS =></span>
<span class="c"> OK tt (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> s.(st_freshreg)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> (AssocMap.set n st s.(st_datapath))</span>
<span class="c"> (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic)))</span>
<span class="c"> (add_instr_state_incr s n n' st STM TRANS)</span>
<span class="c"> | _, _ => Error (Errors.msg "HTL.add_instr")</span>
<span class="c"> end.</span>
<span class="c">Lemma add_instr_skip_state_incr :</span>
<span class="c"> forall s n st,</span>
<span class="c"> (st_datapath s)!n = None -></span>
<span class="c"> (st_controllogic s)!n = None -></span>
<span class="c"> st_incr s</span>
<span class="c"> (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> s.(st_freshreg)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> (AssocMap.set n st s.(st_datapath))</span>
<span class="c"> (AssocMap.set n Vskip s.(st_controllogic))).</span>
<span class="c">Proof.</span>
<span class="c"> constructor; intros;</span>
<span class="c"> try (simpl; destruct (peq n n0); subst);</span>
<span class="c"> auto with htlh.</span>
<span class="c">Qed.</span>
<span class="c">Definition add_instr_skip (n : node) (st : stmnt) : mon unit :=</span>
<span class="c"> fun s =></span>
<span class="c"> match check_empty_node_datapath s n, check_empty_node_controllogic s n with</span>
<span class="c"> | left STM, left TRANS =></span>
<span class="c"> OK tt (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> s.(st_freshreg)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> (AssocMap.set n st s.(st_datapath))</span>
<span class="c"> (AssocMap.set n Vskip s.(st_controllogic)))</span>
<span class="c"> (add_instr_skip_state_incr s n st STM TRANS)</span>
<span class="c"> | _, _ => Error (Errors.msg "HTL.add_instr")</span>
<span class="c"> end.</span>
<span class="c">Lemma add_node_skip_state_incr :</span>
<span class="c"> forall s n st,</span>
<span class="c"> (st_datapath s)!n = None -></span>
<span class="c"> (st_controllogic s)!n = None -></span>
<span class="c"> st_incr s</span>
<span class="c"> (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> s.(st_freshreg)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> (AssocMap.set n Vskip s.(st_datapath))</span>
<span class="c"> (AssocMap.set n st s.(st_controllogic))).</span>
<span class="c">Proof.</span>
<span class="c"> constructor; intros;</span>
<span class="c"> try (simpl; destruct (peq n n0); subst);</span>
<span class="c"> auto with htlh.</span>
<span class="c">Qed.</span>
<span class="c">Definition add_node_skip (n : node) (st : stmnt) : mon unit :=</span>
<span class="c"> fun s =></span>
<span class="c"> match check_empty_node_datapath s n, check_empty_node_controllogic s n with</span>
<span class="c"> | left STM, left TRANS =></span>
<span class="c"> OK tt (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> s.(st_freshreg)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> (AssocMap.set n Vskip s.(st_datapath))</span>
<span class="c"> (AssocMap.set n st s.(st_controllogic)))</span>
<span class="c"> (add_node_skip_state_incr s n st STM TRANS)</span>
<span class="c"> | _, _ => Error (Errors.msg "HTL.add_instr")</span>
<span class="c"> end.</span>
<span class="c">Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e.</span>
<span class="c">Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e.</span>
<span class="c">Definition bop (op : binop) (r1 r2 : reg) : expr :=</span>
<span class="c"> Vbinop op (Vvar r1) (Vvar r2).</span>
<span class="c">Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr :=</span>
<span class="c"> Vbinop op (Vvar r) (Vlit (intToValue l)).</span>
<span class="c">Definition boplitz (op: binop) (r: reg) (l: Z) : expr :=</span>
<span class="c"> Vbinop op (Vvar r) (Vlit (ZToValue l)).</span>
<span class="c">Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr :=</span>
<span class="c"> match c, args with</span>
<span class="c"> | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2)</span>
<span class="c"> | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2)</span>
<span class="c"> | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2)</span>
<span class="c"> | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2)</span>
<span class="c"> | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2)</span>
<span class="c"> | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2)</span>
<span class="c"> | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")</span>
<span class="c"> end.</span>
<span class="c">Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int)</span>
<span class="c"> : mon expr :=</span>
<span class="c"> match c, args with</span>
<span class="c"> | Integers.Ceq, r1::nil => ret (boplit Veq r1 i)</span>
<span class="c"> | Integers.Cne, r1::nil => ret (boplit Vne r1 i)</span>
<span class="c"> | Integers.Clt, r1::nil => ret (boplit Vlt r1 i)</span>
<span class="c"> | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i)</span>
<span class="c"> | Integers.Cle, r1::nil => ret (boplit Vle r1 i)</span>
<span class="c"> | Integers.Cge, r1::nil => ret (boplit Vge r1 i)</span>
<span class="c"> | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")</span>
<span class="c"> end.</span>
<span class="c">Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr :=</span>
<span class="c"> match c, args with</span>
<span class="c"> | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2)</span>
<span class="c"> | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2)</span>
<span class="c"> | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2)</span>
<span class="c"> | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2)</span>
<span class="c"> | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other")</span>
<span class="c"> end.</span>
<span class="c">Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int)</span>
<span class="c"> : mon expr :=</span>
<span class="c"> match c, args with</span>
<span class="c"> | Integers.Clt, r1::nil => ret (boplit Vltu r1 i)</span>
<span class="c"> | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i)</span>
<span class="c"> | Integers.Cle, r1::nil => ret (boplit Vleu r1 i)</span>
<span class="c"> | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i)</span>
<span class="c"> | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other")</span>
<span class="c"> end.</span>
<span class="c">Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :=</span>
<span class="c"> match c, args with</span>
<span class="c"> | Op.Ccomp c, _ => translate_comparison c args</span>
<span class="c"> | Op.Ccompu c, _ => translate_comparisonu c args</span>
<span class="c"> | Op.Ccompimm c i, _ => translate_comparison_imm c args i</span>
<span class="c"> | Op.Ccompuimm c i, _ => translate_comparison_immu c args i</span>
<span class="c"> | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")</span>
<span class="c"> | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero")</span>
<span class="c"> | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other")</span>
<span class="c"> end.</span>
<span class="c">Definition check_address_parameter_signed (p : Z) : bool :=</span>
<span class="c"> Z.leb Integers.Ptrofs.min_signed p</span>
<span class="c"> && Z.leb p Integers.Ptrofs.max_signed.</span>
<span class="c">Definition check_address_parameter_unsigned (p : Z) : bool :=</span>
<span class="c"> Z.leb p Integers.Ptrofs.max_unsigned.</span>
<span class="c">Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=</span>
<span class="c"> match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)</span>
<span class="c"> | Op.Aindexed off, r1::nil =></span>
<span class="c"> if (check_address_parameter_signed off)</span>
<span class="c"> then ret (boplitz Vadd r1 off)</span>
<span class="c"> else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds")</span>
<span class="c"> | Op.Ascaled scale offset, r1::nil =></span>
<span class="c"> if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)</span>
<span class="c"> then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))</span>
<span class="c"> else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds")</span>
<span class="c"> | Op.Aindexed2 offset, r1::r2::nil =></span>
<span class="c"> if (check_address_parameter_signed offset)</span>
<span class="c"> then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))</span>
<span class="c"> else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds")</span>
<span class="c"> | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)</span>
<span class="c"> if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)</span>
<span class="c"> then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))</span>
<span class="c"> else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds")</span>
<span class="c"> | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)</span>
<span class="c"> let a := Integers.Ptrofs.unsigned a in</span>
<span class="c"> if (check_address_parameter_unsigned a)</span>
<span class="c"> then ret (Vlit (ZToValue a))</span>
<span class="c"> else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds")</span>
<span class="c"> | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing")</span>
<span class="c"> end.</span>
<span class="c">(** Translate an instruction to a statement. FIX mulhs mulhu *)</span>
<span class="c">Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=</span>
<span class="c"> match op, args with</span>
<span class="c"> | Op.Omove, r::nil => ret (Vvar r)</span>
<span class="c"> | Op.Ointconst n, _ => ret (Vlit (intToValue n))</span>
<span class="c"> | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r))</span>
<span class="c"> | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)</span>
<span class="c"> | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)</span>
<span class="c"> | Op.Omulimm n, r::nil => ret (boplit Vmul r n)</span>
<span class="c"> | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs")</span>
<span class="c"> | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu")</span>
<span class="c"> | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)</span>
<span class="c"> | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2)</span>
<span class="c"> | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2)</span>
<span class="c"> | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2)</span>
<span class="c"> | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2)</span>
<span class="c"> | Op.Oandimm n, r::nil => ret (boplit Vand r n)</span>
<span class="c"> | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2)</span>
<span class="c"> | Op.Oorimm n, r::nil => ret (boplit Vor r n)</span>
<span class="c"> | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2)</span>
<span class="c"> | Op.Oxorimm n, r::nil => ret (boplit Vxor r n)</span>
<span class="c"> | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r))</span>
<span class="c"> | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2)</span>
<span class="c"> | Op.Oshlimm n, r::nil => ret (boplit Vshl r n)</span>
<span class="c"> | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)</span>
<span class="c"> | Op.Oshrimm n, r::nil => ret (boplit Vshr r n)</span>
<span class="c"> | Op.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm")</span>
<span class="c"> (*ret (Vbinop Vdiv (Vvar r)</span>
<span class="c"> (Vbinop Vshl (Vlit (ZToValue 1))</span>
<span class="c"> (Vlit (intToValue n))))*)</span>
<span class="c"> | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)</span>
<span class="c"> | Op.Oshruimm n, r::nil => ret (boplit Vshru r n)</span>
<span class="c"> | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")</span>
<span class="c"> (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))</span>
<span class="c"> (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)</span>
<span class="c"> | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))</span>
<span class="c"> | Op.Ocmp c, _ => translate_condition c args</span>
<span class="c"> | Op.Osel c AST.Tint, r1::r2::rl =></span>
<span class="c"> do tc <- translate_condition c rl;</span>
<span class="c"> ret (Vternary tc (Vvar r1) (Vvar r2))</span>
<span class="c"> | Op.Olea a, _ => translate_eff_addressing a args</span>
<span class="c"> | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")</span>
<span class="c"> end.</span>
<span class="c">Lemma add_branch_instr_state_incr:</span>
<span class="c"> forall s e n n1 n2,</span>
<span class="c"> (st_datapath s) ! n = None -></span>
<span class="c"> (st_controllogic s) ! n = None -></span>
<span class="c"> st_incr s (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> (st_freshreg s)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> (AssocMap.set n Vskip (st_datapath s))</span>
<span class="c"> (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))).</span>
<span class="c">Proof.</span>
<span class="c"> intros. apply state_incr_intro; simpl;</span>
<span class="c"> try (intros; destruct (peq n0 n); subst);</span>
<span class="c"> auto with htlh.</span>
<span class="c">Qed.</span>
<span class="c">Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=</span>
<span class="c"> fun s =></span>
<span class="c"> match check_empty_node_datapath s n, check_empty_node_controllogic s n with</span>
<span class="c"> | left NSTM, left NTRANS =></span>
<span class="c"> OK tt (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> (st_freshreg s)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> (AssocMap.set n Vskip (st_datapath s))</span>
<span class="c"> (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s)))</span>
<span class="c"> (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS)</span>
<span class="c"> | _, _ => Error (Errors.msg "Htlgen: add_branch_instr")</span>
<span class="c"> end.</span>
<span class="c">Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)</span>
<span class="c"> (args : list reg) (stack : reg) : mon expr :=</span>
<span class="c"> match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)</span>
<span class="c"> | Mint32, Op.Aindexed off, r1::nil =></span>
<span class="c"> if (check_address_parameter_signed off)</span>
<span class="c"> then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))</span>
<span class="c"> else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")</span>
<span class="c"> | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)</span>
<span class="c"> if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)</span>
<span class="c"> then ret (Vvari stack</span>
<span class="c"> (Vbinop Vdivu</span>
<span class="c"> (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))</span>
<span class="c"> (Vlit (ZToValue 4))))</span>
<span class="c"> else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")</span>
<span class="c"> | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)</span>
<span class="c"> let a := Integers.Ptrofs.unsigned a in</span>
<span class="c"> if (check_address_parameter_unsigned a)</span>
<span class="c"> then ret (Vvari stack (Vlit (ZToValue (a / 4))))</span>
<span class="c"> else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset")</span>
<span class="c"> | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing")</span>
<span class="c"> end.</span>
<span class="c">Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) :=</span>
<span class="c"> match ns with</span>
<span class="c"> | n :: ns' => (i, n) :: enumerate (i+1) ns'</span>
<span class="c"> | nil => nil</span>
<span class="c"> end.</span>
<span class="c">Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=</span>
<span class="c"> List.map (fun a => match a with</span>
<span class="c"> (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n)))</span>
<span class="c"> end)</span>
<span class="c"> (enumerate 0 ns).</span>
<span class="c">Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=</span>
<span class="c"> match ni with</span>
<span class="c"> (n, i) =></span>
<span class="c"> match i with</span>
<span class="c"> | Inop n' =></span>
<span class="c"> if Z.leb (Z.pos n') Integers.Int.max_unsigned then</span>
<span class="c"> add_instr n n' Vskip</span>
<span class="c"> else error (Errors.msg "State is larger than 2^32.")</span>
<span class="c"> | Iop op args dst n' =></span>
<span class="c"> if Z.leb (Z.pos n') Integers.Int.max_unsigned then</span>
<span class="c"> do instr <- translate_instr op args;</span>
<span class="c"> do _ <- declare_reg None dst 32;</span>
<span class="c"> add_instr n n' (nonblock dst instr)</span>
<span class="c"> else error (Errors.msg "State is larger than 2^32.")</span>
<span class="c"> | Iload mem addr args dst n' =></span>
<span class="c"> if Z.leb (Z.pos n') Integers.Int.max_unsigned then</span>
<span class="c"> do src <- translate_arr_access mem addr args stack;</span>
<span class="c"> do _ <- declare_reg None dst 32;</span>
<span class="c"> add_instr n n' (nonblock dst src)</span>
<span class="c"> else error (Errors.msg "State is larger than 2^32.")</span>
<span class="c"> | Istore mem addr args src n' =></span>
<span class="c"> if Z.leb (Z.pos n') Integers.Int.max_unsigned then</span>
<span class="c"> do dst <- translate_arr_access mem addr args stack;</span>
<span class="c"> add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *)</span>
<span class="c"> else error (Errors.msg "State is larger than 2^32.")</span>
<span class="c"> | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")</span>
<span class="c"> | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")</span>
<span class="c"> | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")</span>
<span class="c"> | Icond cond args n1 n2 =></span>
<span class="c"> if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then</span>
<span class="c"> do e <- translate_condition cond args;</span>
<span class="c"> add_branch_instr e n n1 n2</span>
<span class="c"> else error (Errors.msg "State is larger than 2^32.")</span>
<span class="c"> | Ijumptable r tbl =></span>
<span class="c"> (*do s <- get;</span>
<span class="c"> add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*)</span>
<span class="c"> error (Errors.msg "Ijumptable: Case statement not supported.")</span>
<span class="c"> | Ireturn r =></span>
<span class="c"> match r with</span>
<span class="c"> | Some r' =></span>
<span class="c"> add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r')))</span>
<span class="c"> | None =></span>
<span class="c"> add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z))))</span>
<span class="c"> end</span>
<span class="c"> end</span>
<span class="c"> end.</span>
<span class="c">Lemma create_reg_state_incr:</span>
<span class="c"> forall s sz i,</span>
<span class="c"> st_incr s (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> (Pos.succ (st_freshreg s))</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))</span>
<span class="c"> s.(st_arrdecls)</span>
<span class="c"> (st_datapath s)</span>
<span class="c"> (st_controllogic s)).</span>
<span class="c">Proof. constructor; simpl; auto with htlh. Qed.</span>
<span class="c">Definition create_reg (i : option io) (sz : nat) : mon reg :=</span>
<span class="c"> fun s => let r := s.(st_freshreg) in</span>
<span class="c"> OK r (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> (Pos.succ r)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls))</span>
<span class="c"> (st_arrdecls s)</span>
<span class="c"> (st_datapath s)</span>
<span class="c"> (st_controllogic s))</span>
<span class="c"> (create_reg_state_incr s sz i).</span>
<span class="c">Lemma create_arr_state_incr:</span>
<span class="c"> forall s sz ln i,</span>
<span class="c"> st_incr s (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> (Pos.succ (st_freshreg s))</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))</span>
<span class="c"> (st_datapath s)</span>
<span class="c"> (st_controllogic s)).</span>
<span class="c">Proof. constructor; simpl; auto with htlh. Qed.</span>
<span class="c">Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) :=</span>
<span class="c"> fun s => let r := s.(st_freshreg) in</span>
<span class="c"> OK (r, ln) (mkstate</span>
<span class="c"> s.(st_st)</span>
<span class="c"> (Pos.succ r)</span>
<span class="c"> (st_freshstate s)</span>
<span class="c"> s.(st_scldecls)</span>
<span class="c"> (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls))</span>
<span class="c"> (st_datapath s)</span>
<span class="c"> (st_controllogic s))</span>
<span class="c"> (create_arr_state_incr s sz ln i).</span>
<span class="c">Definition stack_correct (sz : Z) : bool :=</span>
<span class="c"> (0 <=? sz) && (sz <? Integers.Ptrofs.modulus) && (Z.modulo sz 4 =? 0).</span>
<span class="c">Definition max_pc_map (m : Maps.PTree.t stmnt) :=</span>
<span class="c"> PTree.fold (fun m pc i => Pos.max m pc) m 1%positive.</span>
<span class="c">Lemma max_pc_map_sound:</span>
<span class="c"> forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m).</span>
<span class="c">Proof.</span>
<span class="c"> intros until i. unfold max_pc_function.</span>
<span class="c"> apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m).</span>
<span class="c"> (* extensionality *)</span>
<span class="c"> intros. apply H0. rewrite H; auto.</span>
<span class="c"> (* base case *)</span>
<span class="c"> rewrite PTree.gempty. congruence.</span>
<span class="c"> (* inductive case *)</span>
<span class="c"> intros. rewrite PTree.gsspec in H2. destruct (peq pc k).</span>
<span class="c"> inv H2. xomega.</span>
<span class="c"> apply Ple_trans with a. auto. xomega.</span>
<span class="c">Qed.</span>
<span class="c">Lemma max_pc_wf :</span>
<span class="c"> forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -></span>
<span class="c"> map_well_formed m.</span>
<span class="c">Proof.</span>
<span class="c"> unfold map_well_formed. intros.</span>
<span class="c"> exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x.</span>
<span class="c"> apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B.</span>
<span class="c"> unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst.</span>
<span class="c"> simplify. transitivity (Z.pos (max_pc_map m)); eauto.</span>
<span class="c">Qed.</span>
<span class="c">Definition transf_module (f: function) : mon module :=</span>
<span class="c"> if stack_correct f.(fn_stacksize) then</span>
<span class="c"> do fin <- create_reg (Some Voutput) 1;</span>
<span class="c"> do rtrn <- create_reg (Some Voutput) 32;</span>
<span class="c"> do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4));</span>
<span class="c"> do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));</span>
<span class="c"> do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params);</span>
<span class="c"> do start <- create_reg (Some Vinput) 1;</span>
<span class="c"> do rst <- create_reg (Some Vinput) 1;</span>
<span class="c"> do clk <- create_reg (Some Vinput) 1;</span>
<span class="c"> do current_state <- get;</span>
<span class="c"> match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned,</span>
<span class="c"> zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with</span>
<span class="c"> | left LEDATA, left LECTRL =></span>
<span class="c"> ret (mkmodule</span>
<span class="c"> f.(RTL.fn_params)</span>
<span class="c"> current_state.(st_datapath)</span>
<span class="c"> current_state.(st_controllogic)</span>
<span class="c"> f.(fn_entrypoint)</span>
<span class="c"> current_state.(st_st)</span>
<span class="c"> stack</span>
<span class="c"> stack_len</span>
<span class="c"> fin</span>
<span class="c"> rtrn</span>
<span class="c"> start</span>
<span class="c"> rst</span>
<span class="c"> clk</span>
<span class="c"> current_state.(st_scldecls)</span>
<span class="c"> current_state.(st_arrdecls)</span>
<span class="c"> (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA)))</span>
<span class="c"> | _, _ => error (Errors.msg "More than 2^32 states.")</span>
<span class="c"> end</span>
<span class="c"> else error (Errors.msg "Stack size misalignment.").</span>
<span class="c">Definition max_state (f: function) : state :=</span>
<span class="c"> let st := Pos.succ (max_reg_function f) in</span>
<span class="c"> mkstate st</span>
<span class="c"> (Pos.succ st)</span>
<span class="c"> (Pos.succ (max_pc_function f))</span>
<span class="c"> (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st)))</span>
<span class="c"> (st_arrdecls (init_state st))</span>
<span class="c"> (st_datapath (init_state st))</span>
<span class="c"> (st_controllogic (init_state st)).</span>
<span class="c">Definition transl_module (f : function) : Errors.res module :=</span>
<span class="c"> run_mon (max_state f) (transf_module f).</span>
<span class="c">Definition transl_fundef := transf_partial_fundef transl_module.</span>
<span class="c">(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *)</span>
<span class="c">(*Definition transl_main_fundef f : Errors.res HTL.fundef :=</span>
<span class="c"> match f with</span>
<span class="c"> | Internal f => transl_fundef (Internal f)</span>
<span class="c"> | External f => Errors.Error (Errors.msg "Could not find internal main function")</span>
<span class="c"> end.</span>
<span class="c">(** Translation of a whole program. *)</span>
<span class="c">Definition transl_program (p: RTL.program) : Errors.res HTL.program :=</span>
<span class="c"> transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i</span>
<span class="c"> then transl_fundef f</span>
<span class="c"> else transl_main_fundef f)</span>
<span class="c"> (fun i v => Errors.OK v) p.</span>
<span class="c">*)</span>
<span class="c">Definition main_is_internal (p : RTLBlock.program) : bool :=</span>
<span class="c"> let ge := Globalenvs.Genv.globalenv p in</span>
<span class="c"> match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with</span>
<span class="c"> | Some b =></span>
<span class="c"> match Globalenvs.Genv.find_funct_ptr ge b with</span>
<span class="c"> | Some (AST.Internal _) => true</span>
<span class="c"> | _ => false</span>
<span class="c"> end</span>
<span class="c"> | _ => false</span>
<span class="c"> end.</span>
<span class="c">Definition transl_program (p : RTLBlock.program) : Errors.res HTL.program :=</span>
<span class="c"> if main_is_internal p</span>
<span class="c"> then transform_partial_program transl_fundef p</span>
<span class="c"> else Errors.Error (Errors.msg "Main function is not Internal.").</span>
<span class="c">*)</span></span></span></pre>
</div>
</div></body>
</html>
|
