/
conflicts_modular.v
94 lines (75 loc) 路 2.7 KB
/
conflicts_modular.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
(*! Understanding conflicts and forwarding, with modules !*)
Require Import Koika.Frontend.
Module Import Queue32.
Inductive reg_t := empty | data.
Definition R reg :=
match reg with
| empty => bits_t 1
| data => bits_t 32
end.
Definition dequeue0: UInternalFunction reg_t empty_ext_fn_t :=
{{ fun dequeue0 () : bits_t 32 =>
guard(!read0(empty)); write0(empty, Ob~1); read0(data) }}.
Definition enqueue0: UInternalFunction reg_t empty_ext_fn_t :=
{{ fun enqueue0 (val: bits_t 32) : unit_t =>
guard(read0(empty)); write0(empty, Ob~0); write0(data, val) }}.
Definition dequeue1: UInternalFunction reg_t empty_ext_fn_t :=
{{ fun dequeue1 () : bits_t 32 =>
guard(!read1(empty)); write1(empty, Ob~1); read1(data) }}.
End Queue32.
Inductive reg_t :=
| in0: Queue32.reg_t -> reg_t
| in1: Queue32.reg_t -> reg_t
| fifo: Queue32.reg_t -> reg_t
| out: Queue32.reg_t -> reg_t.
Inductive rule_name_t := deq0 | deq1 | process.
Definition R (reg: reg_t) : type :=
match reg with
| in0 st => Queue32.R st
| in1 st => Queue32.R st
| fifo st => Queue32.R st
| out st => Queue32.R st
end.
Definition urules (rl: rule_name_t) : uaction reg_t empty_ext_fn_t :=
match rl with
| deq0 =>
{{ fifo.(enqueue0)(in0.(dequeue0)()) }}
| deq1 =>
{{ fifo.(enqueue0)(in1.(dequeue0)()) }}
| process =>
{{ out.(enqueue0)(|32`d412| + fifo.(dequeue1)()) }}
end.
Definition rules : rule_name_t -> rule R empty_Sigma :=
tc_rules R empty_Sigma urules.
Definition pipeline : scheduler :=
deq0 |> deq1 |> process |> done.
Definition external (r: rule_name_t) := false.
Definition r (reg: reg_t) : R reg :=
match reg with
| in0 empty => Ob~0
| in0 data => Bits.of_nat _ 42
| in1 empty => Ob~0
| in1 data => Bits.of_nat _ 73
| fifo empty => Ob~1
| fifo data => Bits.zero
| out empty => Ob~1
| out data => Bits.zero
end.
Definition cr := ContextEnv.(create) r.
Definition interp_result :=
tc_compute (commit_update cr (interp_scheduler cr empty_sigma rules pipeline)).
Definition circuits :=
compile_scheduler rules external pipeline.
Definition package :=
{| ip_koika := {| koika_reg_types := R;
koika_reg_init reg := r reg;
koika_ext_fn_types := empty_Sigma;
koika_rules := rules;
koika_rule_external := external;
koika_scheduler := pipeline;
koika_module_name := "conflicts_modular" |};
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 "conflicts_modular.ml" prog.