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
|
From Coq Require Import Lists.List Strings.String.
From Coq Require Import
Structures.OrderedTypeEx
FSets.FMapList
Program.Basics
PeanoNat.
From CoqUp Require Import Helper Tactics.
Import ListNotations.
Module Verilog.
Module Map := FMapList.Make String_as_OT.
Inductive value : Type :=
| VBool (b : bool)
| VArray (l : list value).
Definition cons_value (a b : value) : value :=
match a, b with
| VBool _, VArray b' => VArray (a :: b')
| VArray a', VBool _ => VArray (List.concat [a'; [b]])
| VArray a', VArray b' => VArray (List.concat [a'; b'])
| _, _ => VArray [a; b]
end.
(** * Conversion to and from value *)
Fixpoint nat_to_value' (sz n : nat) : value :=
match sz with
| 0 => VArray []
| S sz' =>
if Nat.even n then
cons_value (VBool false) (nat_to_value' sz' (Nat.div n 2))
else
cons_value (VBool true) (nat_to_value' sz' (Nat.div n 2))
end.
Definition nat_to_value (n : nat) : value :=
nat_to_value' ((Nat.log2 n) + 1) n.
Definition state : Type := Map.t value * Map.t value.
Inductive binop : Type :=
| Plus
| Minus
| Times
| Divide
| LT
| GT
| LE
| GE
| Eq
| And
| Or
| Xor.
Inductive expr : Type :=
| Lit (n : value)
| Var (s : string)
| Neg (a : expr)
| BinOp (op : binop) (a1 a2 : expr)
| Ternary (c t f : expr).
Inductive stmnt : Type :=
| Skip
| Block (s : list stmnt)
| Cond (c : expr) (st sf : stmnt)
| Case (c : expr) (b : list (expr * stmnt))
| Blocking (a b : expr)
| Nonblocking (a b : expr).
Inductive verilog : Type := Verilog (s : list stmnt).
Coercion VBool : bool >-> value.
Coercion Lit : value >-> expr.
Coercion Var : string >-> expr.
Definition value_is_bool (v : value) : bool :=
match v with
| VBool _ => true
| VArray _ => false
end.
Definition value_is_array : value -> bool := compose negb value_is_bool.
Definition flat_value (v : value) : bool :=
match v with
| VBool _ => true
| VArray l => forallb value_is_bool l
end.
Inductive value_is_boolP : value -> Prop :=
| ValIsBool : forall b : bool, value_is_boolP (VBool b).
Inductive value_is_arrayP : value -> Prop :=
| ValIsArray : forall v : list value, value_is_arrayP (VArray v).
Inductive flat_valueP : value -> Prop :=
| FLV0 : forall b : bool, flat_valueP (VBool b)
| FLVA : forall l : list value,
Forall (value_is_boolP) l -> flat_valueP (VArray l).
Lemma value_is_bool_equiv :
forall v, value_is_boolP v <-> value_is_bool v = true.
Proof.
split; intros.
- inversion H. trivial.
- destruct v. constructor. unfold value_is_bool in H. discriminate.
Qed.
Lemma value_is_array_equiv :
forall v, value_is_arrayP v <-> value_is_array v = true.
Proof.
split; intros.
- inversion H. trivial.
- destruct v; try constructor. unfold value_is_array in H.
unfold compose, value_is_bool, negb in H. discriminate.
Qed.
Lemma flat_value_equiv :
forall v, flat_valueP v <-> flat_value v = true.
Proof.
split; intros.
- unfold flat_value. inversion H. subst. trivial.
+ rewrite Forall_forall in H0. rewrite forallb_forall. intros. subst.
apply value_is_bool_equiv. apply H0. assumption.
- destruct v. constructor. constructor. unfold flat_value in H.
rewrite Forall_forall. rewrite forallb_forall in H. intros. apply value_is_bool_equiv.
apply H. assumption.
Qed.
Fixpoint value_to_nat' (i : nat) (v : value) : option nat :=
match i, v with
| _, VBool b => Some (Nat.b2n b)
| _, VArray [VBool b] => Some (Nat.b2n b)
| S i', VArray ((VBool b) :: l) =>
Option.map (compose (Nat.add (Nat.b2n b)) (Mult.tail_mult 2)) (value_to_nat' i' (VArray l))
| _, _ => None
end.
Definition value_length (v : value) : nat :=
match v with
| VBool _ => 1
| VArray l => Datatypes.length l
end.
Definition value_to_nat (v : value) : option nat :=
value_to_nat' (value_length v) v.
Lemma empty_is_flat : flat_valueP (VArray []).
Proof.
constructor. apply Forall_forall. intros. inversion H.
Qed.
Lemma check_5_is_101 :
value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5.
Proof. reflexivity. Qed.
Lemma cons_value_flat :
forall (b : bool) (v : value),
flat_valueP v -> flat_valueP (cons_value (VBool b) v).
Proof.
intros. unfold cons_value. destruct v.
- constructor. apply Forall_forall. intros.
inversion H0; subst. constructor.
inversion H1; subst. constructor.
inversion H2.
- intros. inversion H. inversion H1; subst; constructor.
+ apply Forall_forall. intros.
inversion H0; subst. constructor.
inversion H2.
+ repeat constructor. assumption. assumption.
Qed.
Lemma nat_to_value'_is_flat :
forall (sz n : nat),
flat_valueP (nat_to_value' sz n).
Proof.
induction sz; intros.
- subst. apply empty_is_flat.
- unfold_rec nat_to_value'.
destruct (Nat.even n); apply cons_value_flat; apply IHsz.
Qed.
Lemma nat_to_value_is_flat :
forall (sz n : nat),
flat_valueP (nat_to_value n).
Proof.
intros. unfold nat_to_value. apply nat_to_value'_is_flat.
Qed.
Lemma nat_to_value_idempotent :
forall (sz n : nat),
sz > 0 -> (value_to_nat' sz (nat_to_value' sz n)) = Some n.
Proof.
induction sz; intros.
- inversion H.
- unfold_rec value_to_nat'.
assert (flat_valueP (nat_to_value' (S sz) n)).
{ apply nat_to_value'_is_flat. }
destruct (nat_to_value' (S sz) n) eqn:?.
Admitted.
Module VerilogNotation.
Declare Scope verilog_scope.
Bind Scope verilog_scope with expr.
Bind Scope verilog_scope with stmnt.
Bind Scope verilog_scope with verilog.
Delimit Scope verilog_scope with verilog.
Notation "x + y" := (BinOp Plus x y) (at level 50, left associativity) : verilog_scope.
Notation "x - y" := (BinOp Minus x y) (at level 50, left associativity) : verilog_scope.
Notation "x * y" := (BinOp Times x y) (at level 40, left associativity) : verilog_scope.
Notation "x / y" := (BinOp Divide x y) (at level 40, left associativity) : verilog_scope.
Notation "x < y" := (BinOp LT x y) (at level 70, no associativity) : verilog_scope.
Notation "x <= y" := (BinOp LE x y) (at level 70, no associativity) : verilog_scope.
Notation "x > y" := (BinOp GT x y) (at level 70, no associativity) : verilog_scope.
Notation "x >= y" := (BinOp GE x y) (at level 70, no associativity) : verilog_scope.
Notation "x == y" := (BinOp Eq x y) (at level 70, no associativity) : verilog_scope.
Notation "x & y" := (BinOp And x y) (at level 40, left associativity) : verilog_scope.
Notation "x | y" := (BinOp Eq x y) (at level 40, left associativity) : verilog_scope.
Notation "x ^ y" := (BinOp Eq x y) (at level 30, right associativity) : verilog_scope.
Notation "~ y" := (Neg y) (at level 75, right associativity) : verilog_scope.
Notation "c ? t : f" := (Ternary c t f) (at level 20, right associativity) : verilog_scope.
Notation "a '<=!' b" := (Nonblocking a b) (at level 80, no associativity) : verilog_scope.
Notation "a '=!' b" := (Blocking a b) (at level 80, no associativity) : verilog_scope.
Notation "'IF' c 'THEN' a 'ELSE' b 'FI'" := (Cond c a b) (at level 80, right associativity) : verilog_scope.
End VerilogNotation.
Module VerilogEval.
Definition state_find (k : string) (s : state) : value :=
Option.default (VBool false) (Map.find k (fst s)).
Definition eval_binop (op : binop) (a1 a2 : value) : value :=
match op with
| Plus => a1 + a2
| Minus => a1 - a2
| Times => a1 * a2
end.
Fixpoint eval_expr (s : state) (e : expr) : nat :=
match e with
| Lit n => n
| Var v => state_find v s
| Neg a => 0 - (eval_expr s a)
| BinOp op a1 a2 => eval_binop op a1 a2
| Ternary c t f => if eval_expr s c then eval_expr s t else eval_expr s f
end.
End VerilogEval.
End Verilog.
Export Verilog.
|
