-
Notifications
You must be signed in to change notification settings - Fork 9
/
muxelim.v
102 lines (88 loc) · 3.03 KB
/
muxelim.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
(*! Sanity check for mux-elimination optimization !*)
Require Import Koika.Frontend.
Inductive nested_cnt :=
NC0 | NC1 | NC2 | NC3 | NC4 | NC5 | NC6.
Inductive redundant_cnt :=
RC0 | RC1.
Inductive reg_t :=
| rc_nested (v: nested_cnt)
| rc_redundant (c: redundant_cnt)
| rc_bitwise
| rdata_nested
| rdata_redundant
| rdata_bitwise.
Inductive rule_name_t := rl_nested | rl_redundant | rl_bitwise.
Definition R reg : type :=
match reg with
| rc_nested _ => bits_t 1
| rc_redundant _ => bits_t 1
| rc_bitwise => bits_t 3
| rdata_nested => bits_t 8
| rdata_redundant => bits_t 8
| rdata_bitwise => bits_t 8
end.
Definition r reg : R reg :=
match reg with
| rc_nested _ => Bits.zero
| rc_redundant _ => Bits.zero
| rc_bitwise => Bits.zero
| rdata_nested => Bits.zero
| rdata_redundant => Bits.zero
| rdata_bitwise => Bits.zero
end.
Definition urules rl : uaction reg_t empty_ext_fn_t :=
match rl with
| rl_nested =>
{{ if read0(rc_nested NC0) then
if read0(rc_nested NC1) then
if read0(rc_nested NC2) then pass
else if read0(rc_nested NC3) then
if read0(rc_nested NC4) then pass
else if read0(rc_nested NC5) then
if read0(rc_nested NC6) then
write0(rdata_nested, |8`d24|)
else pass
else pass
else pass
else pass
else pass }}
| rl_redundant =>
{{ if read0(rc_redundant RC0) then
if read0(rc_redundant RC1) then
write1(rdata_redundant, |8`d42|)
else pass
else pass }}
| rl_bitwise =>
{{ match read0(rc_bitwise) with
| Ob~0~1~0 => write0(rdata_bitwise, |8`d0|)
| Ob~1~0~0 => write0(rdata_bitwise, |8`d1|)
| Ob~1~1~0 => write0(rdata_bitwise, |8`d2|)
| Ob~1~1~1 => write0(rdata_bitwise, |8`d3|)
| Ob~0~0~0 => write0(rdata_bitwise, |8`d4|)
return default: fail
end }}
end.
Definition rules :=
tc_rules R empty_Sigma urules.
Definition sched : scheduler :=
rl_nested |> rl_redundant |> rl_bitwise |> 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 := "muxelim" |};
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 "muxelim.ml" prog.