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
|
(*
* CoqUp: Verified high-level synthesis.
* Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
From coqup Require Import HTL Coquplib.
From compcert Require Import Maps.
From compcert Require Errors.
From compcert Require Import AST RTL.
Record state: Type := mkstate {
st_nextinst: positive;
st_instances: instances;
}.
Inductive res (A: Type) (S: Type): Type :=
| Error: Errors.errmsg -> res A S
| OK: A -> S -> res A S.
Arguments OK [A S].
Arguments Error [A S].
Definition mon (A: Type) : Type := res A state.
Definition ret {A: Type} (x: A) (s: state) : mon A := OK x s.
Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B :=
match f with
| Error msg => Error msg
| OK a s => g a
end.
Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C :=
bind f (fun xy => g (fst xy) (snd xy)).
Definition bindS {A B: Type} (f: mon A) (g: A -> state -> mon B) : mon B :=
match f with
| Error msg => Error msg
| OK a s => g a s
end.
Notation "'do' X <- A ; B" := (bind A (fun X => B))
(at level 200, X ident, A at level 100, B at level 200).
Notation "'do' ( X , Y ) <- A ; B" := (bindS A (fun X Y => B))
(at level 200, X ident, Y ident, A at level 100, B at level 200).
Definition handle_error {A: Type} (f g: mon A) : mon A :=
match f with
| OK a s' => OK a s'
| Error _ => g
end.
Definition init_state : state :=
mkstate 1%positive empty_instances.
Module PTree.
Export Maps.PTree.
Fixpoint xtraverse {A B : Type} (f : positive -> A -> state -> mon B)
(m : PTree.t A) (s : state) (i : positive)
{struct m} : mon (PTree.t B) :=
match m with
| Leaf => OK Leaf s
| Node l o r =>
let newo :=
match o with
| None => OK None s
| Some x =>
match f (prev i) x s with
| Error err => Error err
| OK val s' => OK (Some val) s'
end
end in
match newo with
| OK no s =>
do (nl, s') <- xtraverse f l s (xO i);
do (nr, s'') <- xtraverse f r s' (xI i);
OK (Node nl no nr) s''
| Error msg => Error msg
end
end.
Definition traverse {A B : Type} (f : positive -> A -> state -> mon B) m :=
xtraverse f m init_state xH.
Definition traverse1 {A B : Type} (f : A -> state -> mon B) := traverse (fun _ => f).
End PTree.
Definition transf_instr (pc: node) (rtl: RTL.instruction) (s: state)
: mon HTL.instruction :=
match rtl with
| RTL.Inop n =>
(** Nop instruction should just become a Skip in Verilog, which is just a
semicolon. *)
ret (HTL.Hnop n) s
| RTL.Iop op args res n =>
(** Perform an arithmetic operation over registers. This will just become
one binary operation in Verilog. This will contain a list of registers,
so these will just become a chain of binary operations in Verilog. *)
ret (HTL.Hnonblock op args res n) s
| RTL.Iload chunk addr args dst n =>
(** Load from memory, which will maybe become a load from RAM, however, I'm
not sure yet how memory will be implemented or how it will formalised
be. *)
ret (HTL.Hload chunk addr args dst n) s
| RTL.Istore chunk addr args src n =>
(** How memory will be laid out will also affect how stores are handled. For
now hopefully these can be ignored, and hopefull they are not used that
often when they are not required in C. *)
ret (HTL.Hstore chunk addr args src n) s
| RTL.Icall sig ros args res n =>
(** Function call should become a module instantiation with start and end
signals appropriately wired up. *)
match ros with
| inr i =>
let inst := mkinst i args in
let newinstances := PTree.set s.(st_nextinst) inst s.(st_instances) in
ret (HTL.Hinst sig i res n)
(mkstate ((s.(st_nextinst) + 1)%positive)
newinstances)
| _ => Error (Errors.msg "Function pointers are not supported.")
end
| RTL.Itailcall sig ros args =>
(** Should be converted into a reset of the modules state, setting the
initial variables correctly. This would simulate a tailcall as it is
similar to jumping back to the top of the function in assembly. *)
match ros with
| inr i => ret (HTL.Htailcall sig i args) s
| _ => Error (Errors.msg "Function pointers are not supported.")
end
| RTL.Ibuiltin ef args res n =>
(** Builtin functions will have to supported manually, by implementing the
Verilog myself. *)
Error (Errors.msg "builtin functions are not supported.")
| RTL.Icond cond args n1 n2 =>
(** Will be converted into two separate processes that are combined by a mux
at the end, with a start flag that propagates in the construct that should
be chosen. *)
ret (HTL.Hcond cond args n1 n2) s
| RTL.Ijumptable arg tbl =>
(** A jump to a specific instruction in the list, this will require setting
the state in the state machine appropriately. This is trivial to
implement if no scheduling is involved, but as soon as that isn't the
case it might be difficult to find that location. It would help to
transform the CFG to a few basic blocks first which cannot have any
branching. *)
ret (HTL.Hjumptable arg tbl) s
| RTL.Ireturn r =>
(** The return value of the function, which will just mean that the finished
signal goes high and the result is stored in the result register. *)
ret (HTL.Hfinish r) s
end.
Definition transf_function (f: function) : Errors.res module :=
match (PTree.traverse transf_instr f.(fn_code)) with
| OK code s =>
Errors.OK (mkmodule
f.(fn_sig)
f.(fn_params)
f.(fn_stacksize)
code
s.(st_instances)
f.(fn_entrypoint))
| Error err => Errors.Error err
end.
Definition transf_fundef (fd: fundef) : Errors.res moddecl :=
transf_partial_fundef transf_function fd.
Definition transf_program (p: program) : Errors.res design :=
transform_partial_program transf_fundef p.
|
