forked from mit-plv/koika
-
Notifications
You must be signed in to change notification settings - Fork 1
/
shifts.v
156 lines (127 loc) · 7.7 KB
/
shifts.v
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
(*! Regression test for signed shifts !*)
Require Import Koika.Frontend.
Inductive idx := r3 | r4 | r5 | r6 | r7 | r8 | r9 | r10 | r11 | r12 | r13 | r14 | r15 | r16.
Inductive reg_t := cond | r_l (_: idx) | r_r (_: idx) | r_out (_: idx).
Inductive rule_name_t := rl.
Definition R (reg: reg_t) : type :=
match reg with
| cond => bits_t 1
| _ => bits_t 32
end.
Definition r (reg: reg_t) : R reg :=
match reg with
| cond => Ob~1
| r_l r3 => Ob~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0
| r_r r3 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1
| r_l r4 => Ob~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0
| r_r r4 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1
| r_l r5 => Ob~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0
| r_r r5 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~0
| r_l r6 => Ob~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1
| r_r r6 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1
| r_l r7 => Ob~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1
| r_r r7 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0
| r_l r8 => Ob~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1
| r_r r8 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1
| r_l r9 => Ob~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1
| r_r r9 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1
| r_l r10 => Ob~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1
| r_r r10 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~0
| r_l r11 => Ob~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1
| r_r r11 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1
| r_l r12 => Ob~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1
| r_r r12 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0
| r_l r13 => Ob~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1
| r_r r13 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1
| r_l r14 => Ob~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1
| r_r r14 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1
| r_l r15 => Ob~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1
| r_r r15 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~0
| r_l r16 => Ob~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1
| r_r r16 => Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1
| r_out _ => Bits.zero
end.
Definition urules (rl: rule_name_t) : uaction reg_t empty_ext_fn_t :=
{{
write0(r_out r3, if read0(cond)
then (read0(r_l r3) >>> read0(r_r r3)) >>> read0(r_r r3)
else (read0(r_l r3) >> read0(r_r r3)) >> read0(r_r r3));
(* Ob~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0 *)
write0(r_out r4, if read0(cond)
then (read0(r_l r4) >>> read0(r_r r4)) >>> read0(r_r r4)
else (read0(r_l r4) >> read0(r_r r4)) >> read0(r_r r4));
(* Ob~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0 *)
write0(r_out r5, if read0(cond)
then (read0(r_l r5) >>> read0(r_r r5)) >>> read0(r_r r5)
else (read0(r_l r5) >> read0(r_r r5)) >> read0(r_r r5));
(* Ob~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0 *)
write0(r_out r6, if read0(cond)
then (read0(r_l r6) >>> read0(r_r r6)) >>> read0(r_r r6)
else (read0(r_l r6) >> read0(r_r r6)) >> read0(r_r r6));
(* Ob~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 *)
write0(r_out r7, if read0(cond)
then (read0(r_l r7) >>> read0(r_r r7)) >>> read0(r_r r7)
else (read0(r_l r7) >> read0(r_r r7)) >> read0(r_r r7));
(* Ob~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 *)
write0(r_out r8, if read0(cond)
then (read0(r_l r8) >>> read0(r_r r8)) >>> read0(r_r r8)
else (read0(r_l r8) >> read0(r_r r8)) >> read0(r_r r8));
(* Ob~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 *)
write0(r_out r9, if read0(cond)
then (read0(r_l r9) >>> read0(r_r r9)) >>> read0(r_r r9)
else (read0(r_l r9) >> read0(r_r r9)) >> read0(r_r r9));
(* Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 *)
write0(r_out r10, if read0(cond)
then (read0(r_l r10) >>> read0(r_r r10)) >>> read0(r_r r10)
else (read0(r_l r10) >> read0(r_r r10)) >> read0(r_r r10));
(* Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1 *)
write0(r_out r11, if read0(cond)
then (read0(r_l r11) >>> read0(r_r r11)) >>> read0(r_r r11)
else (read0(r_l r11) >> read0(r_r r11)) >> read0(r_r r11));
(* Ob~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0 *)
write0(r_out r12, if read0(cond)
then (read0(r_l r12) >>> read0(r_r r12)) >>> read0(r_r r12)
else (read0(r_l r12) >> read0(r_r r12)) >> read0(r_r r12));
(* Ob~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1 *)
write0(r_out r13, if read0(cond)
then (read0(r_l r13) >>> read0(r_r r13)) >>> read0(r_r r13)
else (read0(r_l r13) >> read0(r_r r13)) >> read0(r_r r13));
(* Ob~1~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0 *)
write0(r_out r14, if read0(cond)
then (read0(r_l r14) >>> read0(r_r r14)) >>> read0(r_r r14)
else (read0(r_l r14) >> read0(r_r r14)) >> read0(r_r r14));
(* Ob~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~1~1~0~0~0~0~0~0~1~1~0 *)
write0(r_out r15, if read0(cond)
then (read0(r_l r15) >>> read0(r_r r15)) >>> read0(r_r r15)
else (read0(r_l r15) >> read0(r_r r15)) >> read0(r_r r15));
(* Ob~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0 *)
write0(r_out r16, if read0(cond)
then (read0(r_l r16) >>> read0(r_r r16)) >>> read0(r_r r16)
else (read0(r_l r16) >> read0(r_r r16)) >> read0(r_r r16));
(* Ob~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1 *)
write0(cond, !read0(cond))
}}.
Definition rules :=
tc_rules R empty_Sigma urules.
Definition sched : scheduler :=
rl |> done.
Definition sched_result :=
tc_compute (interp_scheduler (ContextEnv.(create) r) empty_sigma rules sched).
Definition external (r: rule_name_t) := false.
Definition sched_circuits :=
compile_scheduler rules external sched.
Definition sched_circuits_result :=
tc_compute (interp_circuits empty_sigma sched_circuits (lower_r (ContextEnv.(create) r))).
Definition package :=
{| ip_koika := {| koika_reg_types := R;
koika_reg_init := r;
koika_ext_fn_types := empty_Sigma;
koika_rules := rules;
koika_rule_external := external;
koika_scheduler := sched;
koika_module_name := "shifts" |};
ip_sim := {| sp_ext_fn_specs := empty_ext_fn_props;
sp_prelude := None |};
ip_verilog := {| vp_ext_fn_specs := empty_ext_fn_props |} |}.
Definition prog := Interop.Backends.register package.
Extraction "shifts.ml" prog.