diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | README.md | 6 | ||||
| -rw-r--r-- | driver/CoqupDriver.ml | 75 | ||||
| -rw-r--r-- | src/Compiler.v | 4 | ||||
| -rw-r--r-- | src/Simulator.v | 32 | ||||
| -rw-r--r-- | src/common/Coquplib.v | 11 | ||||
| -rw-r--r-- | src/extraction/Extraction.v | 6 | ||||
| -rw-r--r-- | src/translation/Veriloggen.v | 128 | ||||
| -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 |
12 files changed, 798 insertions, 158 deletions
@@ -12,7 +12,7 @@ COQMAKE := "$(COQBIN)coq_makefile" COQUPDIRS := translation common verilog VSSUBDIR := $(foreach d, $(COQUPDIRS), src/$(d)/*.v) -VS := src/Compiler.v $(VSSUBDIR) +VS := src/Compiler.v src/Simulator.v $(VSSUBDIR) PREFIX ?= . @@ -73,7 +73,7 @@ Which will install the binary in `./bin/coqup` by default. However, this can be To test out `coqup` you can try the following examples which are in the test folder using the following: ``` shell -./bin/coqup --hls test/loop.c -o loop.v -./bin/coqup --hls test/conditional.c -o conditional.v -./bin/coqup --hls test/add.c -o add.v +./bin/coqup test/loop.c -o loop.v +./bin/coqup test/conditional.c -o conditional.v +./bin/coqup test/add.c -o add.v ``` diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml index 0a4f84f..80b4145 100644 --- a/driver/CoqupDriver.ml +++ b/driver/CoqupDriver.ml @@ -1,5 +1,15 @@ -(* - * CoqUp: Verified high-level synthesis. +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) +(* CoqUp: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify @@ -17,6 +27,7 @@ *) open Printf +open Coqup.Camlcoq open Coqup.Commandline open Coqup.Clflags open Coqup.CommonOptions @@ -28,6 +39,7 @@ open Coqup.Linker open Coqup.Diagnostics (* Coqup flags *) +let option_simulate = ref false let option_hls = ref true (* Name used for version string etc. *) @@ -37,7 +49,7 @@ let tool_name = "C verified high-level synthesis" let sdump_suffix = ref ".json" let nolink () = - !option_c || !option_S || !option_E || !option_interp + !option_c || !option_S || !option_E || !option_interp || !option_hls let object_filename sourcename suff = if nolink () then @@ -63,17 +75,47 @@ let compile_c_file sourcename ifile ofile = set_dest Coqup.AsmToJSON.destination option_sdump !sdump_suffix; (* Parse the ast *) let csyntax = parse_c_file sourcename ifile in - (* Convert to Asm *) - let verilog = - match Coqup.Compiler0.transf_hls csyntax with - | Coqup.Errors.OK v -> + if not !option_hls then begin + (* Convert to Asm *) + let asm = + match Coqup.Compiler.apply_partial + (Coqup.Compiler.transf_c_program csyntax) + Coqup.Asmexpand.expand_program with + | Coqup.Errors.OK asm -> + asm + | Coqup.Errors.Error msg -> + let loc = file_loc sourcename in + fatal_error loc "%a" print_error msg in + (* Dump Asm in binary and JSON format *) + Coqup.AsmToJSON.print_if asm sourcename; + (* Print Asm in text form *) + let oc = open_out ofile in + Coqup.PrintAsm.print_program oc asm; + close_out oc + end else begin + let verilog = + match Coqup.Compiler0.transf_hls csyntax with + | Coqup.Errors.OK v -> v - | Coqup.Errors.Error msg -> - let loc = file_loc sourcename in + | Coqup.Errors.Error msg -> + let loc = file_loc sourcename in fatal_error loc "%a" print_error msg in - let oc = open_out ofile in - Coqup.PrintVerilog.print_program oc verilog; - close_out oc + if not !option_simulate then begin + let oc = open_out ofile in + Coqup.PrintVerilog.print_program oc verilog; + close_out oc + end else begin + print_endline "Simulating"; + let result = + match Coqup.Simulator.simulate (Nat.of_int 100) verilog with + | Coqup.Errors.OK r -> r + | Coqup.Errors.Error msg -> + let loc = file_loc sourcename in + fatal_error loc "%a" print_error msg in + printf "Length: %d\n" (List.length result); + Coqup.PrintVerilog.print_result result + end + end (* From C source to asm *) @@ -83,7 +125,7 @@ let compile_i_file sourcename preproname = let csyntax = parse_c_file sourcename preproname in Coqup.Interp.execute csyntax; "" - end else if !option_S then begin + end else if !option_hls then begin compile_c_file sourcename preproname (output_filename ~final:true sourcename ".c" ".v"); "" @@ -183,6 +225,7 @@ Processing options: -S Compile to assembler only, save result in <file>.s -o <file> Generate output in <file> --no-hls Do not use HLS and generate standard flow. + --simulate Simulate the result with the Verilog semantics. |} ^ prepro_help ^ language_support_help ^ @@ -281,7 +324,9 @@ let cmdline_actions = Exact "-help", Unit print_usage_and_exit; Exact "--help", Unit print_usage_and_exit;] @ (* Use HLS *) - [Exact "--no-hls", Unset option_hls;] + [Exact "--no-hls", Unset option_hls; + Exact "--simulate", Set option_simulate; + ] (* Getting version info *) @ version_options tool_name @ (* Enforcing CompCert build numbers for QSKs and mnemonics dump *) @@ -294,7 +339,7 @@ let cmdline_actions = (* Processing options *) [ Exact "-c", Set option_c; Exact "-E", Set option_E; - Exact "--hls", Set option_S; + Exact "-S", Set option_S; Exact "-o", String(fun s -> option_o := Some s); Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in option_o := Some s);] diff --git a/src/Compiler.v b/src/Compiler.v index 5b4ef0a..697732d 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -1,4 +1,4 @@ -(* +(* -*- mode: coq -*- * CoqUp: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * @@ -74,7 +74,7 @@ Proof. intros. destruct x; simpl. rewrite print_identity. auto. auto. Qed. -Definition transf_backend (r : RTL.program) : res Verilog.module := +Definition transf_backend (r : RTL.program) : res Verilog.module := OK r @@@ Veriloggen.transf_program. diff --git a/src/Simulator.v b/src/Simulator.v new file mode 100644 index 0000000..3c5aca0 --- /dev/null +++ b/src/Simulator.v @@ -0,0 +1,32 @@ +(* -*- 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/>. + *) + +From Coq Require Import FSets.FMapPositive. + +From compcert Require Import Errors. + +From coqup Require Compiler Verilog Value. +From coqup Require Import Coquplib. + +Local Open Scope error_monad_scope. + +Definition simulate (n : nat) (m : Verilog.module) : res (list (positive * Value.value)) := + do map <- Verilog.module_run n m; + OK (PositiveMap.elements map). + +Local Close Scope error_monad_scope. diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 666d740..47360d6 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -65,6 +65,17 @@ Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : o | _ => None end. +Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B := + match f with + | Some a => g a + | _ => None + end. + +Module Notation. +Notation "'do' X <- A ; B" := (bind A (fun X => B)) + (at level 200, X ident, A at level 100, B at level 200). +End Notation. + End Option. Parameter debug_print : string -> unit. diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index ff0b8ba..319e2eb 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -1,4 +1,4 @@ -(* +(* -*- mode: coq -*- * CoqUp: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> * @@ -16,7 +16,7 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From coqup Require Verilog Compiler. +From coqup Require Verilog Value Compiler Simulator. From Coq Require DecidableClass. @@ -166,7 +166,7 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction - Verilog.module Verilog.valueToZ coqup.Compiler.transf_hls + Verilog.module Value.uvalueToZ coqup.Compiler.transf_hls Simulator.simulate Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index f0620bf..6aa94df 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -1,4 +1,4 @@ -(* +(* -*- mode: coq -*- * CoqUp: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * @@ -18,7 +18,7 @@ From Coq Require Import FSets.FMapPositive. -From coqup Require Import Verilog Coquplib. +From coqup Require Import Verilog Coquplib Value. From compcert Require Errors Op AST Integers Maps. From compcert Require Import RTL. @@ -29,6 +29,11 @@ Definition node : Type := positive. Definition reg : Type := positive. Definition ident : Type := positive. +Hint Resolve PositiveMap.gempty : verilog_state. +Hint Resolve PositiveMap.gso : verilog_state. +Hint Resolve PositiveMap.gss : verilog_state. +Hint Resolve Ple_refl : verilog_state. + Inductive statetrans : Type := | StateGoto (p : node) | StateCond (c : expr) (t f : node). @@ -36,11 +41,13 @@ Inductive statetrans : Type := Definition valid_freshstate (stm: PositiveMap.t stmnt) (fs: node) := forall (n: node), Plt n fs \/ stm!n = None. +Hint Unfold valid_freshstate : verilog_state. Definition states_have_transitions (stm: PositiveMap.t stmnt) (st: PositiveMap.t statetrans) := forall (n: node), (forall x, stm!n = Some x -> exists y, st!n = Some y) /\ (forall x, st!n = Some x -> exists y, stm!n = Some y). +Hint Unfold states_have_transitions : verilog_state. Record state: Type := mkstate { st_freshreg: reg; @@ -54,7 +61,8 @@ Record state: Type := mkstate { Remark init_state_valid_freshstate: valid_freshstate (PositiveMap.empty stmnt) 1%positive. -Proof. intros. right. apply PositiveMap.gempty. Qed. +Proof. auto with verilog_state. Qed. +Hint Resolve init_state_valid_freshstate : verilog_state. Remark init_state_states_have_transitions: states_have_transitions (PositiveMap.empty stmnt) (PositiveMap.empty statetrans). @@ -62,11 +70,12 @@ Proof. unfold states_have_transitions. split; intros; rewrite PositiveMap.gempty in H; discriminate. Qed. +Hint Resolve init_state_states_have_transitions : verilog_state. Remark init_state_wf: valid_freshstate (PositiveMap.empty stmnt) 1%positive /\ states_have_transitions (PositiveMap.empty stmnt) (PositiveMap.empty statetrans). -Proof. split; intros. apply init_state_valid_freshstate. apply init_state_states_have_transitions. Qed. +Proof. auto with verilog_state. Qed. Definition init_state : state := mkstate 1%positive @@ -87,27 +96,24 @@ Inductive state_incr: state -> state -> Prop := s1.(st_statetrans)!n = None \/ s2.(st_statetrans)!n = s1.(st_statetrans)!n) -> state_incr s1 s2. +Hint Constructors state_incr : verilog_state. Lemma state_incr_refl: forall s, state_incr s s. -Proof. intros. apply state_incr_intro; - try (apply Ple_refl); - try (intros; right; reflexivity). -Qed. +Proof. auto with verilog_state. Qed. Lemma state_incr_trans: forall s1 s2 s3, state_incr s1 s2 -> state_incr s2 s3 -> state_incr s1 s3. Proof. - intros. inv H. inv H0. apply state_incr_intro. - - apply Ple_trans with (st_freshreg s2); assumption. - - apply Ple_trans with (st_freshstate s2); assumption. + intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans. - intros. destruct H3 with n. - + left. assumption. - + destruct H6 with n. - * rewrite <- H0. left. assumption. - * right. rewrite <- H0. apply H8. + + left; assumption. + + destruct H6 with n; + [ rewrite <- H0; left; assumption + | right; rewrite <- H0; apply H8 + ]. - intros. destruct H4 with n. - + left. assumption. + + left; assumption. + destruct H7 with n. * rewrite <- H0. left. assumption. * right. rewrite <- H0. apply H8. @@ -280,6 +286,7 @@ Proof. rewrite PositiveMap.gso. apply (st_wf s). assumption. Qed. +Hint Resolve add_instr_valid_freshstate : verilog_state. Remark add_instr_states_have_transitions: forall (s: state) (n n': node) (st: stmnt), @@ -299,6 +306,7 @@ Proof. assert (H2 := st_wf s). inv H2. unfold states_have_transitions in H1. destruct H1 with n0. apply H3 with x. assumption. assumption. assumption. Qed. +Hint Resolve add_instr_states_have_transitions : verilog_state. Remark add_instr_state_wf: forall (s: state) (n n': node) (st: stmnt) (LT: Plt n (st_freshstate s)), @@ -306,10 +314,7 @@ Remark add_instr_state_wf: /\ states_have_transitions (PositiveMap.add n st s.(st_stm)) (PositiveMap.add n (StateGoto n') s.(st_statetrans)). -Proof. - split; intros. apply add_instr_valid_freshstate. assumption. - apply add_instr_states_have_transitions. -Qed. +Proof. auto with verilog_state. Qed. Lemma add_instr_state_incr : forall s n n' st LT, @@ -323,9 +328,9 @@ Lemma add_instr_state_incr : s.(st_decl) (add_instr_state_wf s n n' st LT)). Proof. - intros. apply state_incr_intro; intros; simpl; try reflexivity; - destruct (peq n n0); try (subst; left; assumption); - right; apply PositiveMap.gso; apply not_eq_sym; assumption. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with verilog_state. Qed. Definition check_empty_node_stm: @@ -365,9 +370,7 @@ Definition add_reg (r: reg) (s: state) : state := Lemma add_reg_state_incr: forall r s, state_incr s (add_reg r s). -Proof. - intros. apply state_incr_intro; unfold add_reg; try right; reflexivity. -Qed. +Proof. auto with verilog_state. Qed. Definition add_instr_reg (r: reg) (n: node) (n': node) (st: stmnt) : mon unit := do _ <- map_state (add_reg r) (add_reg_state_incr r); @@ -382,9 +385,7 @@ Lemma change_decl_state_incr: (st_statetrans s) decl' (st_wf s)). -Proof. - intros. apply state_incr_intro; simpl; try reflexivity; right; reflexivity. -Qed. +Proof. auto with verilog_state. Qed. Lemma decl_io_state_incr: forall s, @@ -395,10 +396,7 @@ Lemma decl_io_state_incr: (st_statetrans s) (st_decl s) (st_wf s)). -Proof. - intros. apply state_incr_intro; try right; try reflexivity. - simpl. apply Ple_succ. -Qed. +Proof. constructor; simpl; auto using Ple_succ with verilog_state. Qed. Definition decl_io (sz: nat): mon (reg * nat) := fun s => let r := s.(st_freshreg) in @@ -430,17 +428,10 @@ Lemma add_branch_instr_states_have_transitions: states_have_transitions (PositiveMap.add n Vskip (st_stm s)) (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s)). Proof. - split; intros. - - destruct (peq n0 n). - + subst. exists (StateCond e n1 n2). apply PositiveMap.gss. - + rewrite PositiveMap.gso. rewrite PositiveMap.gso in H. - assert (H1 := (st_wf s)). inv H1. unfold states_have_transitions in H2. - destruct H2 with n0. apply H1 with x. assumption. assumption. assumption. - - destruct (peq n0 n). - + subst. exists Vskip. apply PositiveMap.gss. - + rewrite PositiveMap.gso. rewrite PositiveMap.gso in H. - assert (H1 := (st_wf s)). inv H1. unfold states_have_transitions in H2. - destruct H2 with n0. apply H3 with x. assumption. assumption. assumption. + split; intros; destruct (peq n0 n); subst; eauto with verilog_state; + rewrite PositiveMap.gso in *; + assert (H1 := (st_wf s)); inv H1; unfold states_have_transitions in H2; + destruct H2 with n0; try (apply H1 with x); try (apply H3 with x); assumption. Qed. Lemma add_branch_valid_freshstate: @@ -448,11 +439,10 @@ Lemma add_branch_valid_freshstate: Plt n (st_freshstate s) -> valid_freshstate (PositiveMap.add n Vskip (st_stm s)) (st_freshstate s). Proof. - unfold valid_freshstate. intros. destruct (peq n0 n). - - subst. left. assumption. - - assert (H1 := st_wf s). destruct H1. - unfold valid_freshstate in H0. rewrite PositiveMap.gso. apply H0. - assumption. + unfold valid_freshstate; intros; destruct (peq n0 n). + - subst; auto. + - assert (H1 := st_wf s); destruct H1; + unfold valid_freshstate in H0; rewrite PositiveMap.gso; auto. Qed. Lemma add_branch_instr_st_wf: @@ -462,8 +452,7 @@ Lemma add_branch_instr_st_wf: /\ states_have_transitions (PositiveMap.add n Vskip (st_stm s)) (PositiveMap.add n (StateCond e n1 n2) (st_statetrans s)). Proof. - split; intros. apply add_branch_valid_freshstate. assumption. - apply add_branch_instr_states_have_transitions. + auto using add_branch_valid_freshstate, add_branch_instr_states_have_transitions. Qed. Lemma add_branch_instr_state_incr: @@ -478,8 +467,9 @@ Lemma add_branch_instr_state_incr: (st_decl s) (add_branch_instr_st_wf s e n n1 n2 LT)). Proof. - intros. apply state_incr_intro; simpl; try reflexivity; intros; destruct (peq n0 n); - try (subst; left; assumption); right; apply PositiveMap.gso; assumption. + intros. apply state_incr_intro; simpl; + try (intros; destruct (peq n0 n); subst); + auto with verilog_state. Qed. Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := @@ -517,27 +507,27 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit := | Ireturn r => match r with | Some r' => - add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)) :: block rtrn (Vvar r') :: nil)) + add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r'))) | None => - add_instr n n (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z)) :: nil)) + add_instr n n (block fin (Vlit (ZToValue 1%nat 1%Z))) end end end. Definition make_stm_cases (s : positive * stmnt) : expr * stmnt := - match s with (a, b) => (posToExpr a, b) end. + match s with (a, b) => (posToExpr 32 a, b) end. Definition make_stm (r : reg) (s : PositiveMap.t stmnt) : stmnt := - Vcase (Vvar r) (map make_stm_cases (PositiveMap.elements s)). + Vcase (Vvar r) (map make_stm_cases (PositiveMap.elements s)) (Some Vskip). Definition make_statetrans_cases (r : reg) (st : positive * statetrans) : expr * stmnt := match st with - | (n, StateGoto n') => (posToExpr n, nonblock r (posToExpr n')) - | (n, StateCond c n1 n2) => (posToExpr n, nonblock r (Vternary c (posToExpr n1) (posToExpr n2))) + | (n, StateGoto n') => (posToExpr 32 n, nonblock r (posToExpr 32 n')) + | (n, StateCond c n1 n2) => (posToExpr 32 n, nonblock r (Vternary c (posToExpr 32 n1) (posToExpr 32 n2))) end. Definition make_statetrans (r : reg) (s : PositiveMap.t statetrans) : stmnt := - Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)). + Vcase (Vvar r) (map (make_statetrans_cases r) (PositiveMap.elements s)) (Some Vskip). Fixpoint allocate_regs (e : list (reg * nat)) {struct e} : list module_item := match e with @@ -546,11 +536,11 @@ Fixpoint allocate_regs (e : list (reg * nat)) {struct e} : list module_item := end. Definition make_module_items (entry: node) (clk st rst: reg) (s: state) : list module_item := - (Valways (Voredge (Vposedge clk) (Vposedge rst)) - (Vcond (Vbinop Veq (Vvar rst) (Vlit (ZToValue 1%nat 1%Z))) - (nonblock st (posToExpr entry)) + (Valways_ff (Vposedge clk) + (Vcond (Vbinop Veq (Vinputvar rst) (Vlit (ZToValue 1 1))) + (nonblock st (posToExpr 32 entry)) (make_statetrans st s.(st_statetrans)))) - :: (Valways Valledge (make_stm st s.(st_stm))) + :: (Valways_ff (Vposedge clk) (make_stm st s.(st_stm))) :: (allocate_regs (PositiveMap.elements s.(st_decl))). (** To start out with, the assumption is made that there is only one @@ -584,18 +574,14 @@ Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef Lemma max_state_valid_freshstate: forall f, valid_freshstate (st_stm init_state) (Pos.succ (max_pc_function f)). -Proof. - unfold valid_freshstate. intros. right. simpl. apply PositiveMap.gempty. -Qed. +Proof. unfold valid_freshstate; simpl; auto with verilog_state. Qed. +Hint Resolve max_state_valid_freshstate : verilog_state. Lemma max_state_st_wf: forall f, valid_freshstate (st_stm init_state) (Pos.succ (max_pc_function f)) /\ states_have_transitions (st_stm init_state) (st_statetrans init_state). -Proof. - split. apply max_state_valid_freshstate. - apply init_state_states_have_transitions. -Qed. +Proof. auto with verilog_state. Qed. Definition max_state (f: function) : state := mkstate (Pos.succ (max_reg_function f)) 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. + +*) |