diff options
Diffstat (limited to 'src/verilog')
-rw-r--r-- | src/verilog/PrintVerilog.ml | 78 | ||||
-rw-r--r-- | src/verilog/PrintVerilog.mli | 2 | ||||
-rw-r--r-- | src/verilog/Value.v | 217 | ||||
-rw-r--r-- | src/verilog/Verilog.v | 395 |
4 files changed, 629 insertions, 63 deletions
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml index 292fcf2..17c0b16 100644 --- a/src/verilog/PrintVerilog.ml +++ b/src/verilog/PrintVerilog.ml @@ -1,4 +1,4 @@ -(* +(* -*- mode: tuareg -*- * CoqUp: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * @@ -17,6 +17,7 @@ *) open Verilog +open Value open Datatypes open Camlcoq @@ -31,23 +32,32 @@ let fold_map f s = List.map f s |> concat let pstr pp = fprintf pp "%s" -let pprint_binop = function - | Vadd -> " + " - | Vsub -> " - " - | Vmul -> " * " - | Vdiv -> " / " - | Vmod -> " % " - | Vlt -> " < " - | Vgt -> " > " - | Vle -> " <= " - | Vge -> " >= " - | Veq -> " == " - | Vne -> " != " - | Vand -> " & " - | Vor -> " | " - | Vxor -> " ^ " - | Vshl -> " << " - | Vshr -> " >> " +let pprint_binop l r = + let unsigned op = sprintf "{%s %s %s}" l op r in + let signed op = sprintf "{$signed(%s) %s $signed(%s)}" l op r in + function + | Vadd -> unsigned "+" + | Vsub -> unsigned "-" + | Vmul -> unsigned "*" + | Vdiv -> signed "/" + | Vdivu -> unsigned "/" + | Vmod -> signed "%" + | Vmodu -> unsigned "%" + | Vlt -> signed "<" + | Vltu -> unsigned "<" + | Vgt -> signed ">" + | Vgtu -> unsigned ">" + | Vle -> signed "<=" + | Vleu -> unsigned "<=" + | Vge -> signed ">=" + | Vgeu -> unsigned ">=" + | Veq -> unsigned "==" + | Vne -> unsigned "!=" + | Vand -> unsigned "&" + | Vor -> unsigned "|" + | Vxor -> unsigned "^" + | Vshl -> unsigned "<<" + | Vshr -> unsigned ">>" let unop = function | Vneg -> " ~ " @@ -55,25 +65,29 @@ let unop = function let register a = sprintf "reg_%d" (P.to_int a) -let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l)) +let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l)) let rec pprint_expr = function | Vlit l -> literal l | Vvar s -> register s + | Vinputvar s -> register s | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] - | Vbinop (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"] + | Vbinop (op, a, b) -> concat ["("; pprint_binop (pprint_expr a) (pprint_expr b) op; ")"] | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] let rec pprint_stmnt i = - let pprint_case (e, s) = concat [indent (i + 1); pprint_expr e; ":\n"; pprint_stmnt (i + 2) s] + let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s; + indent (i + 1); "end\n" + ] in function | Vskip -> concat [indent i; ";\n"] - | Vseq s -> concat [indent i; "begin\n"; fold_map (pprint_stmnt (i+1)) s; indent i; "end\n"] - | Vcond (e, st, sf) -> concat [ indent i; "if ("; pprint_expr e; ")\n"; - pprint_stmnt (i + 1) st; indent i; "else\n"; - pprint_stmnt (i + 1) sf + | Vseq (s1, s2) -> concat [ pprint_stmnt i s1; pprint_stmnt i s2] + | Vcond (e, st, sf) -> concat [ indent i; "if ("; pprint_expr e; ") begin\n"; + pprint_stmnt (i + 1) st; indent i; "end else begin\n"; + pprint_stmnt (i + 1) sf; + indent i; "end\n" ] - | Vcase (e, es) -> concat [ indent i; "case ("; pprint_expr e; ")\n"; + | Vcase (e, es, d) -> concat [ indent i; "case ("; pprint_expr e; ")\n"; fold_map pprint_case es; indent (i+1); "default:;\n"; indent i; "endcase\n" ] @@ -97,10 +111,15 @@ let declare i t = concat [ indent i; t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; register r; ";\n" ] +(* TODO Fix always blocks, as they currently always print the same. *) let pprint_module_item i = function | Vdecl (r, sz) -> declare i "reg" (r, sz) | Valways (e, s) -> concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + | Valways_ff (e, s) -> + concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + | Valways_comb (e, s) -> + concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] let rec intersperse c = function | [] -> [] @@ -154,3 +173,10 @@ let pprint_module i n m = ] let print_program pp v = pstr pp (pprint_module 0 "main" v) + +let rec print_result = + function + | [] -> () + | (r, v) :: ls -> + printf "%s -> %s\n" (register r) (literal v); + print_result ls diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli index 181a9d2..b4d2937 100644 --- a/src/verilog/PrintVerilog.mli +++ b/src/verilog/PrintVerilog.mli @@ -17,3 +17,5 @@ *) val print_program : out_channel -> Verilog.coq_module -> unit + +val print_result : (BinNums.positive * Value.value) list -> unit diff --git a/src/verilog/Value.v b/src/verilog/Value.v new file mode 100644 index 0000000..be6babf --- /dev/null +++ b/src/verilog/Value.v @@ -0,0 +1,217 @@ +(* -*- mode: coq -*- + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +(* begin hide *) +From bbv Require Import Word. +From Coq Require Import ZArith.ZArith. +From compcert Require Import lib.Integers. +(* end hide *) + +(** * Value + +A [value] is a bitvector with a specific size. We are using the implementation +of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse. +However, we need to wrap it with an [Inductive] so that we can specify and match +on the size of the [value]. This is necessary so that we can easily store +[value]s of different sizes in a list or in a map. + +Using the default [word], this would not be possible, as the size is part of the type. *) + +Record value : Type := + mkvalue { + vsize: nat; + vword: word vsize + }. + +(** ** Value conversions + +Various conversions to different number types such as [N], [Z], [positive] and +[int], where the last one is a theory of integers of powers of 2 in CompCert. *) + +Definition wordToValue : forall sz : nat, word sz -> value := mkvalue. + +Definition valueToWord : forall v : value, word (vsize v) := vword. + +Definition valueToNat (v : value) : nat := + wordToNat (vword v). + +Definition natToValue sz (n : nat) : value := + mkvalue sz (natToWord sz n). + +Definition valueToN (v : value) : N := + wordToN (vword v). + +Definition NToValue sz (n : N) : value := + mkvalue sz (NToWord sz n). + +Definition posToValue sz (p : positive) : value := + mkvalue sz (posToWord sz p). + +Definition posToValueAuto (p : positive) : value := + let size := Z.to_nat (Z.succ (log_inf p)) in + mkvalue size (Word.posToWord size p). + +Definition ZToValue (s : nat) (z : Z) : value := + mkvalue s (ZToWord s z). + +Definition valueToZ (v : value) : Z := + wordToZ (vword v). + +Definition uvalueToZ (v : value) : Z := + uwordToZ (vword v). + +Definition intToValue (i : Integers.int) : value := + ZToValue Int.wordsize (Int.unsigned i). + +(** Convert a [value] to a [bool], so that choices can be made based on the +result. This is also because comparison operators will give back [value] instead +of [bool], so if they are in a condition, they will have to be converted before +they can be used. *) + +Definition valueToBool (v : value) : bool := + negb (weqb (@wzero (vsize v)) (vword v)). + +Definition boolToValue (sz : nat) (b : bool) : value := + natToValue sz (if b then 1 else 0). + +(** ** Arithmetic operations *) + +Lemma unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. +Proof. intros; subst; assumption. Qed. + +Definition value_eq_size: + forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. +Proof. + intros; destruct (Nat.eqb (vsize v1) (vsize v2)) eqn:?. + left; apply Nat.eqb_eq in Heqb; assumption. + right; trivial. +Defined. + +Definition value_eq_size_nat: + forall (sz : nat) (v : value), { sz = vsize v } + { True }. +Proof. + intros; destruct (Nat.eqb sz (vsize v)) eqn:?. + left; apply Nat.eqb_eq in Heqb; assumption. + right; trivial. +Defined. + +Definition map_any {A : Type} (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) + (EQ : vsize v1 = vsize v2) : A := + let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in + f (vword v1) w2. + +Definition map_any_opt {A : Type} (sz : nat) (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) + : option A := + match value_eq_size v1 v2 with + | left EQ => + Some (map_any v1 v2 f EQ) + | _ => None + end. + +Definition map_word (f : forall sz : nat, word sz -> word sz) (v : value) : value := + mkvalue (vsize v) (f (vsize v) (vword v)). + +Definition map_word2 (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) + (EQ : (vsize v1 = vsize v2)) : value := + let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in + mkvalue (vsize v1) (f (vsize v1) (vword v1) w2). + +Definition map_word2_opt (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) + : option value := + match value_eq_size v1 v2 with + | left EQ => Some (map_word2 f v1 v2 EQ) + | _ => None + end. + +Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value) + : option value := + match value_eq_size v1 v2 with + | left EQ => Some (f EQ) + | _ => None + end. + +(** Arithmetic operations over [value], interpreting them as signed or unsigned +depending on the operation. + +The arithmetic operations over [word] are over [N] by default, however, can also +be called over [Z] explicitly, which is where the bits are interpreted in a +signed manner. *) + +Definition vplus v1 v2 := map_word2 wplus v1 v2. +Definition vminus v1 v2 := map_word2 wminus v1 v2. +Definition vmul v1 v2 := map_word2 wmult v1 v2. +Definition vdiv v1 v2 := map_word2 wdiv v1 v2. +Definition vmod v1 v2 := map_word2 wmod v1 v2. + +Definition vmuls v1 v2 := map_word2 wmultZ v1 v2. +Definition vdivs v1 v2 := map_word2 wdivZ v1 v2. +Definition vmods v1 v2 := map_word2 wremZ v1 v2. + +(** ** Bitwise operations + +Bitwise operations over [value], which is independent of whether the number is +signed or unsigned. *) + +Definition vnot v := map_word wnot v. +Definition vneg v := map_word wneg v. +Definition vbitneg v := boolToValue (vsize v) (negb (valueToBool v)). +Definition vor v1 v2 := map_word2 wor v1 v2. +Definition vand v1 v2 := map_word2 wand v1 v2. +Definition vxor v1 v2 := map_word2 wxor v1 v2. + +(** ** Comparison operators + +Comparison operators that return a bool, there should probably be an equivalent +which returns another number, however I might just add that as an explicit +conversion. *) + +Definition veqb v1 v2 := map_any v1 v2 (@weqb (vsize v1)). +Definition vneb v1 v2 EQ := negb (veqb v1 v2 EQ). + +Definition veq v1 v2 EQ := boolToValue (vsize v1) (veqb v1 v2 EQ). +Definition vne v1 v2 EQ := boolToValue (vsize v1) (vneb v1 v2 EQ). + +Definition vltb v1 v2 := map_any v1 v2 wltb. +Definition vleb v1 v2 EQ := negb (map_any v2 v1 wltb (eq_sym EQ)). +Definition vgtb v1 v2 EQ := map_any v2 v1 wltb (eq_sym EQ). +Definition vgeb v1 v2 EQ := negb (map_any v1 v2 wltb EQ). + +Definition vltsb v1 v2 := map_any v1 v2 wsltb. +Definition vlesb v1 v2 EQ := negb (map_any v2 v1 wsltb (eq_sym EQ)). +Definition vgtsb v1 v2 EQ := map_any v2 v1 wsltb (eq_sym EQ). +Definition vgesb v1 v2 EQ := negb (map_any v1 v2 wsltb EQ). + +Definition vlt v1 v2 EQ := boolToValue (vsize v1) (vltb v1 v2 EQ). +Definition vle v1 v2 EQ := boolToValue (vsize v1) (vleb v1 v2 EQ). +Definition vgt v1 v2 EQ := boolToValue (vsize v1) (vgtb v1 v2 EQ). +Definition vge v1 v2 EQ := boolToValue (vsize v1) (vgeb v1 v2 EQ). + +Definition vlts v1 v2 EQ := boolToValue (vsize v1) (vltsb v1 v2 EQ). +Definition vles v1 v2 EQ := boolToValue (vsize v1) (vlesb v1 v2 EQ). +Definition vgts v1 v2 EQ := boolToValue (vsize v1) (vgtsb v1 v2 EQ). +Definition vges v1 v2 EQ := boolToValue (vsize v1) (vgesb v1 v2 EQ). + +(** ** Shift operators + +Shift operators on values. *) + +Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz) := + f w1 (wordToNat w2). + +Definition vshl v1 v2 := map_word2 (fun sz => shift_map sz (@wlshift sz)) v1 v2. +Definition vshr v1 v2 := map_word2 (fun sz => shift_map sz (@wrshift sz)) v1 v2. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index b9200b7..61df580 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -1,4 +1,4 @@ -(* +(* -*- mode: coq -*- * CoqUp: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * @@ -21,38 +21,44 @@ From Coq Require Import FSets.FMapPositive Program.Basics PeanoNat - ZArith. + ZArith + Lists.List + Program. -From bbv Require Word. +Import ListNotations. -From coqup.common Require Import Coquplib Show. +From coqup Require Import common.Coquplib common.Show verilog.Value. From compcert Require Integers. +From compcert Require Import Errors. -Import ListNotations. +Notation "a ! b" := (PositiveMap.find b a) (at level 1). Definition reg : Type := positive. +Definition node : Type := positive. Definition szreg : Type := reg * nat. -Record value : Type := mkvalue { - vsize : nat; - vword : Word.word vsize -}. +Definition assoclist : Type := PositiveMap.t value. -Definition posToValue (p : positive) : value := - let size := Z.to_nat (Z.succ (log_inf p)) in - mkvalue size (Word.posToWord size p). +(** * Verilog AST -Definition ZToValue (s : nat) (z : Z) : value := - mkvalue s (Word.ZToWord s z). +The Verilog AST is defined here, which is the target language of the +compilation. -Definition intToValue (i : Integers.int) : value := - mkvalue 32%nat (Word.ZToWord 32%nat (Integers.Int.unsigned i)). +** Value -Definition valueToZ (v : value) : Z := - Word.uwordToZ v.(vword). +The Verilog [value] is a bitvector containg a size and the actual bitvector. In +this case, the [Word.word] type is used as many theorems about that bitvector +have already been proven. *) -Definition state : Type := PositiveMap.t value * PositiveMap.t value. +Definition estate : Type := assoclist * assoclist. + +(** ** Binary Operators + +These are the binary operations that can be represented in Verilog. Ideally, +multiplication and division would be done by custom modules which could al so be +scheduled properly. However, for now every Verilog operator is assumed to take +one clock cycle. *) Inductive binop : Type := | Vadd : binop (** addition (binary [+]) *) @@ -61,7 +67,7 @@ Inductive binop : Type := | Vdiv : binop (** division (binary [/]) *) | Vdivu : binop (** division unsigned (binary [/]) *) | Vmod : binop (** remainder ([%]) *) -| Vmodu : binop (** remainder unsigned ([/]) *) +| Vmodu : binop (** remainder unsigned ([%]) *) | Vlt : binop (** less than ([<]) *) | Vltu : binop (** less than unsigned ([<]) *) | Vgt : binop (** greater than ([>]) *) @@ -76,49 +82,75 @@ Inductive binop : Type := | Vor : binop (** or (binary [|]) *) | Vxor : binop (** xor (binary [^|]) *) | Vshl : binop (** shift left ([<<]) *) -| Vshr : binop. (** shift left ([<<]) *) +| Vshr : binop. (** shift right ([>>]) *) + +(** ** Unary Operators *) Inductive unop : Type := | Vneg (** negation ([~]) *) | Vnot. (** not operation [!] *) +(** ** Expressions *) + Inductive expr : Type := | Vlit : value -> expr | Vvar : reg -> expr +| Vinputvar : reg -> expr | Vbinop : binop -> expr -> expr -> expr | Vunop : unop -> expr -> expr | Vternary : expr -> expr -> expr -> expr. -Definition posToExpr (p : positive) : expr := - Vlit (posToValue p). +Definition posToExpr (sz : nat) (p : positive) : expr := + Vlit (posToValue sz p). + +(** ** Statements *) Inductive stmnt : Type := | Vskip : stmnt -| Vseq : list stmnt -> stmnt +| Vseq : stmnt -> stmnt -> stmnt | Vcond : expr -> stmnt -> stmnt -> stmnt -| Vcase : expr -> list (expr * stmnt) -> stmnt +| Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt | Vblock : expr -> expr -> stmnt | Vnonblock : expr -> expr -> stmnt. -(** [edge] is not part of [stmnt] in this formalisation because is closer to the - semantics that are used. *) +(** ** Edges + +These define when an always block should be triggered, for example if the always +block should be triggered synchronously at the clock edge, or asynchronously for +combinational logic. + +[edge] is not part of [stmnt] in this formalisation because is closer to the +semantics that are used. *) + Inductive edge : Type := | Vposedge : reg -> edge | Vnegedge : reg -> edge | Valledge : edge | Voredge : edge -> edge -> edge. +(** ** Module Items + +Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). +The declarations are always register declarations as combinational logic can be +done using combinational always block instead of continuous assignments. *) + Inductive module_item : Type := | Vdecl : reg -> nat -> module_item -| Valways : edge -> stmnt -> module_item. - -(** [mod_start] If set, starts the computations in the module. *) -(** [mod_reset] If set, reset the state in the module. *) -(** [mod_clk] The clock that controls the computation in the module. *) -(** [mod_args] The arguments to the module. *) -(** [mod_finish] Bit that is set if the result is ready. *) -(** [mod_return] The return value that was computed. *) -(** [mod_body] The body of the module, including the state machine. *) +| Valways : edge -> stmnt -> module_item +| Valways_ff : edge -> stmnt -> module_item +| Valways_comb : edge -> stmnt -> module_item. + +(** The main module type containing all the important control signals + +- [mod_start] If set, starts the computations in the module. +- [mod_reset] If set, reset the state in the module. +- [mod_clk] The clock that controls the computation in the module. +- [mod_args] The arguments to the module. +- [mod_finish] Bit that is set if the result is ready. +- [mod_return] The return value that was computed. +- [mod_body] The body of the module, including the state machine. +*) + Record module : Type := mkmodule { mod_start : szreg; mod_reset : szreg; @@ -132,7 +164,296 @@ Record module : Type := mkmodule { (** Convert a [positive] to an expression directly, setting it to the right size. *) Definition posToLit (p : positive) : expr := - Vlit (posToValue p). + Vlit (posToValueAuto p). Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. + +Inductive state: Type := +| State: + forall (assoc: assoclist) + (nbassoc: assoclist), + state +| Callstate: state +| Returnstate: state. + +Definition fext := reg -> res value. +Definition fextclk := nat -> fext. + +Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value := + match op with + | Vadd => vplus + | Vsub => vminus + | Vmul => vmul + | Vdiv => vdivs + | Vdivu => vdiv + | Vmod => vmods + | Vmodu => vmod + | Vlt => vlts + | Vltu => vlt + | Vgt => vgts + | Vgtu => vgt + | Vle => vles + | Vleu => vle + | Vge => vges + | Vgeu => vge + | Veq => veq + | Vne => vne + | Vand => vand + | Vor => vor + | Vxor => vxor + | Vshl => vshl + | Vshr => vshr + end. + +Definition unop_run (op : unop) : value -> value := + match op with + | Vneg => vnot + | Vnot => vbitneg + end. + +Inductive expr_runp : assoclist -> expr -> value -> Prop := + | erun_Vlit : + forall a v, + expr_runp a (Vlit v) v + | erun_Vvar : + forall assoc v r, + assoc!r = Some v -> + expr_runp assoc (Vvar r) v + | erun_Vbinop : + forall a op l r lv rv oper EQ, + expr_runp a l lv -> + expr_runp a r rv -> + oper = binop_run op -> + expr_runp a (Vbinop op l r) (oper lv rv EQ) + | erun_Vunop : + forall a u vu op oper, + expr_runp a u vu -> + oper = unop_run op -> + expr_runp a (Vunop op u) (oper vu) + | erun_Vternary_true : + forall a c t f vc vt, + expr_runp a c vc -> + expr_runp a t vt -> + valueToBool vc = true -> + expr_runp a (Vternary c t f) vt + | erun_Vternary_false : + forall a c t f vc vf, + expr_runp a c vc -> + expr_runp a f vf -> + valueToBool vc = false -> + expr_runp a (Vternary c t f) vf. + +Definition handle_opt {A : Type} (err : errmsg) (val : option A) + : res A := + match val with + | Some a => OK a + | None => Error err + end. + +Definition handle_def {A : Type} (a : A) (val : option A) + : res A := + match val with + | Some a' => OK a' + | None => OK a + end. + +Local Open Scope error_monad_scope. + +(* TODO FIX Vvar case without default *) +Fixpoint expr_run (f : fext) (assoc : assoclist) (e : expr) + {struct e} : res value := + match e with + | Vlit v => OK v + | Vvar r => handle_def (ZToValue 32 0) assoc!r + | Vinputvar r => f r + | Vbinop op l r => + let lv := expr_run f assoc l in + let rv := expr_run f assoc r in + let oper := binop_run op in + do lv' <- lv; + do rv' <- rv; + handle_opt (msg "Verilog: sizes are not equal") + (eq_to_opt lv' rv' (oper lv' rv')) + | Vunop op e => + let oper := unop_run op in + do ev <- expr_run f assoc e; + OK (oper ev) + | Vternary c te fe => + do cv <- expr_run f assoc c; + if valueToBool cv then expr_run f assoc te else expr_run f assoc fe + end. + +(** Return the name of the lhs of an assignment. For now, this function is quite +simple because only assignment to normal variables is supported and needed. *) + +Definition assign_name (e : expr) : res reg := + match e with + | Vvar r => OK r + | _ => Error (msg "Verilog: expression not supported on lhs of assignment") + end. + +Fixpoint find_case_stmnt (f : fext) (a : assoclist) (v : value) (cl : list (expr * stmnt)) + {struct cl} : option (res stmnt) := + match cl with + | (e, s)::xs => + match expr_run f a e with + | OK v' => + match eq_to_opt v v' (veq v v') with + | Some eq => if valueToBool eq then Some (OK s) else find_case_stmnt f a v xs + | None => Some (Error (msg "Verilog: equality check sizes not equal")) + end + | Error msg => Some (Error msg) + end + | _ => None + end. + +Fixpoint stmnt_run' (f : fext) (n : nat) (s : state) (st : stmnt) {struct n} : res state := + match n with + | S n' => + match st with + | Vskip => OK s + | Vseq s1 s2 => + do s' <- stmnt_run' f n' s s1; + stmnt_run' f n' s' s2 + | Vcond c st sf => + match s with + | State assoc _ => + do cv <- expr_run f assoc c; + if valueToBool cv + then stmnt_run' f n' s st + else stmnt_run' f n' s sf + | _ => Error (msg "Verilog: stmnt execution in wrong state") + end + | Vcase e cl defst => + match s with + | State a _ => + do v <- expr_run f a e; + match find_case_stmnt f a v cl with + | Some (OK st') => stmnt_run' f n' s st' + | Some (Error msg) => Error msg + | None => do s' <- handle_opt (msg "Verilog: no case was matched") + (option_map (stmnt_run' f n' s) defst); s' + end + | _ => Error (msg "Verilog: stmnt execution in wrong state") + end + | Vblock lhs rhs => + match s with + | State assoc nbassoc => + do name <- assign_name lhs; + do rhse <- expr_run f assoc rhs; + OK (State (PositiveMap.add name rhse assoc) nbassoc) + | _ => Error (msg "Verilog: stmnt exectution in wrong state") + end + | Vnonblock lhs rhs => + match s with + | State assoc nbassoc => + do name <- assign_name lhs; + do rhse <- expr_run f assoc rhs; + OK (State assoc (PositiveMap.add name rhse nbassoc)) + | _ => Error (msg "Verilog: stmnt execution in wrong state") + end + end + | _ => OK s + end. + +Fixpoint stmnt_height (st : stmnt) {struct st} : nat := + match st with + | Vskip => 1 + | Vseq s1 s2 => stmnt_height s1 + stmnt_height s2 + | Vcond _ s1 s2 => Nat.max (stmnt_height s1) (stmnt_height s2) + | Vcase _ ls (Some st) => + fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls + | _ => 1 + end. + +Definition stmnt_run (f : fext) (s : state) (st : stmnt) : res state := + stmnt_run' f (stmnt_height st) s st. + +Fixpoint mi_step (f : fext) (s : state) (m : list module_item) {struct m} : res state := + let run := fun st ls => + do s' <- stmnt_run f s st; + mi_step f s' ls + in + match m with + | (Valways _ st)::ls => run st ls + | (Valways_ff _ st)::ls => run st ls + | (Valways_comb _ st)::ls => run st ls + | (Vdecl _ _)::ls => mi_step f s ls + | nil => OK s + end. + +Definition add_assoclist (r : reg) (v : value) (assoc : assoclist) : assoclist := + PositiveMap.add r v assoc. + +Definition merge_assoclist (nbassoc assoc : assoclist) : assoclist := + PositiveMap.fold add_assoclist nbassoc assoc. + +Definition empty_assoclist : assoclist := PositiveMap.empty value. + +Definition mi_step_commit (f : fext) (assoc : assoclist) (m : list module_item) : res assoclist := + match mi_step f (State assoc empty_assoclist) m with + | OK (State assoc' nbassoc) => + OK (merge_assoclist nbassoc assoc') + | Error msg => Error msg + | _ => Error (msg "Returned in the wrong state") + end. + +Fixpoint mi_run (f : fextclk) (assoc : assoclist) (m : list module_item) (n : nat) + {struct n} : res assoclist := + match n with + | S n' => + do assoc' <- mi_step_commit (f n') assoc m; + mi_run f assoc' m n' + | O => OK assoc + end. + +Definition module_run (n : nat) (m : module) : res assoclist := + let f := + fun n => + match n with + | 1%nat => fun r => if Pos.eqb r (fst (mod_reset m)) then OK (natToValue 1 1) else Error (msg "") + | _ => fun r => if Pos.eqb r (fst (mod_reset m)) then OK (natToValue 1 0) else Error (msg "") + end in + mi_run f empty_assoclist (mod_body m) n. + +Local Close Scope error_monad_scope. + +(*Theorem value_eq_size_if_eq: + forall lv rv EQ, + vsize lv = vsize rv -> value_eq_size lv rv = left EQ. +Proof. intros. unfold value_eq_size. + +Theorem expr_run_same: + forall assoc e v, expr_run assoc e = OK v <-> expr_runp assoc e v. +Proof. + split; generalize dependent v; generalize dependent assoc. + - induction e. + + intros. inversion H. constructor. + + intros. inversion H. constructor. assumption. + + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (expr_run assoc e2) eqn:?. + unfold eq_to_opt in H1. destruct (value_eq_size v0 v1) eqn:?. inversion H1. + constructor. apply IHe1. assumption. apply IHe2. assumption. reflexivity. discriminate. discriminate. + discriminate. + + intros. inversion H. destruct (expr_run assoc e) eqn:?. unfold option_map in H1. + inversion H1. constructor. apply IHe. assumption. reflexivity. discriminate. + + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (valueToBool v0) eqn:?. + eapply erun_Vternary_true. apply IHe1. eassumption. apply IHe2. eassumption. assumption. + eapply erun_Vternary_false. apply IHe1. eassumption. apply IHe3. eassumption. assumption. + discriminate. + - induction e. + + intros. inversion H. reflexivity. + + intros. inversion H. subst. simpl. assumption. + + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. + apply IHe2 in H6. rewrite H6. unfold eq_to_opt. assert (vsize lv = vsize rv). + apply EQ. apply (value_eq_size_if_eq lv rv EQ) in H0. rewrite H0. reflexivity. + + intros. inversion H. subst. simpl. destruct (expr_run assoc e) eqn:?. simpl. + apply IHe in H3. rewrite Heqo in H3. + inversion H3. subst. reflexivity. apply IHe in H3. rewrite Heqo in H3. discriminate. + + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. + apply IHe2 in H6. rewrite H6. reflexivity. + subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe3. + assumption. +Qed. + +*) |