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
|
From Coq Require Import Lists.List Strings.String.
From Coq Require Import
Structures.OrderedTypeEx
FSets.FMapList
Program.Basics.
From CoqUp Require Import Helper.
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' =>
match Nat.modulo n 2 with
| 0 => cons_value (VBool false) (nat_to_value sz' (Nat.div n 2))
| S _ => cons_value (VBool true) (nat_to_value sz' (Nat.div n 2))
end
end.
Coercion VBool : bool >-> value.
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 : value, value_is_boolP b -> flat_valueP 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.
destruct v.
+ trivial.
+ inversion H0.
+ subst. rewrite Forall_forall in H0. rewrite forallb_forall.
intros. apply value_is_bool_equiv. apply H0. assumption.
- unfold flat_value in H. destruct v.
+ repeat constructor.
+ constructor. apply value_is_bool_equiv. rewrite forallb_forall in H.
Fixpoint value_to_nat (v : value) : option nat :=
match v with
| VBool b => 0
| VArray (l :: ls) =>
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.
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 :=
opt_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.
|
