diff options
Diffstat (limited to 'src/hls/Verilog.v')
-rw-r--r-- | src/hls/Verilog.v | 893 |
1 files changed, 893 insertions, 0 deletions
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v new file mode 100644 index 0000000..e5f86d5 --- /dev/null +++ b/src/hls/Verilog.v @@ -0,0 +1,893 @@ +(* + * Vericert: 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 + * 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 + Structures.OrderedTypeEx + FSets.FMapPositive + Program.Basics + PeanoNat + ZArith + Lists.List + Program. + +Require Import Lia. + +Import ListNotations. + +From vericert Require Import Vericertlib Show ValueInt AssocMap Array. +From compcert Require Events. +From compcert Require Import Integers Errors Smallstep Globalenvs. + +Local Open Scope assocmap. + +Set Implicit Arguments. + +Definition reg : Type := positive. +Definition node : Type := positive. +Definition szreg : Type := reg * nat. + +Record associations (A : Type) : Type := + mkassociations { + assoc_blocking : AssocMap.t A; + assoc_nonblocking : AssocMap.t A + }. + +Definition arr := (Array (option value)). + +Definition reg_associations := associations value. +Definition arr_associations := associations arr. + +Definition assocmap_reg := AssocMap.t value. +Definition assocmap_arr := AssocMap.t arr. + +Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg := + AssocMapExt.merge value new old. + +Definition merge_cell (new : option value) (old : option value) : option value := + match new, old with + | Some _, _ => new + | _, _ => old + end. + +Definition merge_arr (new : option arr) (old : option arr) : option arr := + match new, old with + | Some new', Some old' => Some (combine merge_cell new' old') + | Some new', None => Some new' + | None, Some old' => Some old' + | None, None => None + end. + +Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr := + AssocMap.combine merge_arr new old. + +Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := + match a ! r with + | None => None + | Some arr => Some (Option.default (NToValue 0) (Option.join (array_get_error i arr))) + end. + +Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := + match a ! r with + | None => a + | Some arr => a # r <- (array_set i (Some v) arr) + end. + +Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := + mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking). + +Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := + mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)). + +Definition block_reg (r : reg) (asr : reg_associations) (v : value) := + mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking). + +Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := + mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). + +Inductive scl_decl : Type := VScalar (sz : nat). +Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). + +(** * Verilog AST + +The Verilog AST is defined here, which is the target language of the +compilation. + +** Value + +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. *) + +(** ** 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 [+]) *) +| Vsub : binop (** subtraction (binary [-]) *) +| Vmul : binop (** multiplication (binary [*]) *) +| Vdiv : binop (** division (binary [/]) *) +| Vdivu : binop (** division unsigned (binary [/]) *) +| Vmod : binop (** remainder ([%]) *) +| Vmodu : binop (** remainder unsigned ([%]) *) +| Vlt : binop (** less than ([<]) *) +| Vltu : binop (** less than unsigned ([<]) *) +| Vgt : binop (** greater than ([>]) *) +| Vgtu : binop (** greater than unsigned ([>]) *) +| Vle : binop (** less than or equal ([<=]) *) +| Vleu : binop (** less than or equal unsigned ([<=]) *) +| Vge : binop (** greater than or equal ([>=]) *) +| Vgeu : binop (** greater than or equal unsigned ([>=]) *) +| Veq : binop (** equal to ([==]) *) +| Vne : binop (** not equal to ([!=]) *) +| Vand : binop (** and (binary [&]) *) +| Vor : binop (** or (binary [|]) *) +| Vxor : binop (** xor (binary [^|]) *) +| Vshl : binop (** shift left ([<<]) *) +| Vshr : binop (** shift right ([>>>]) *) +| Vshru : binop. (** shift right unsigned ([>>]) *) +(*| Vror : binop (** shift right unsigned ([>>]) *)*) + +(** ** Unary Operators *) + +Inductive unop : Type := +| Vneg (** negation ([-]) *) +| Vnot. (** not operation [!] *) + +(** ** Expressions *) + +Inductive expr : Type := +| Vlit : value -> expr +| Vvar : reg -> expr +| Vvari : reg -> expr -> 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). + +(** ** Statements *) + +Inductive stmnt : Type := +| Vskip : stmnt +| Vseq : stmnt -> stmnt -> stmnt +| Vcond : expr -> stmnt -> stmnt -> stmnt +| Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt +| Vblock : expr -> expr -> stmnt +| Vnonblock : expr -> expr -> stmnt. + +(** ** 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 io : Type := +| Vinput : io +| Voutput : io +| Vinout : io. + +Inductive declaration : Type := +| Vdecl : option io -> reg -> nat -> declaration +| Vdeclarr : option io -> reg -> nat -> nat -> declaration. + +Inductive module_item : Type := +| Vdeclaration : declaration -> module_item +| 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 : reg; + mod_reset : reg; + mod_clk : reg; + mod_finish : reg; + mod_return : reg; + mod_st : reg; (**r Variable that defines the current state, it should be internal. *) + mod_stk : reg; + mod_stk_len : nat; + mod_args : list reg; + mod_body : list module_item; + mod_entrypoint : node; +}. + +Definition fundef := AST.fundef module. + +Definition program := AST.program fundef unit. + +(** Convert a [positive] to an expression directly, setting it to the right + size. *) +Definition posToLit (p : positive) : expr := + Vlit (posToValue p). + +Definition fext := unit. +Definition fextclk := nat -> fext. + +(** ** State + +The [state] contains the following items: +n +- Current [module] that is being worked on, so that the state variable can be +retrieved and set appropriately. +- Current [module_item] which is being worked on. +- A contiunation ([cont]) which defines what to do next. The option is to + either evaluate another module item or go to the next clock cycle. Finally + it could also end if the finish flag of the module goes high. +- Association list containing the blocking assignments made, or assignments made + in previous clock cycles. +- Nonblocking association list containing all the nonblocking assignments made + in the current module. +- The environment containing values for the input. +- The program counter which determines the value for the state in this version of + Verilog, as the Verilog was generated by the RTL, which means that we have to + make an assumption about how it looks. In this case, that it contains state + which determines which part of the Verilog is executed. This is then the part + of the Verilog that should match with the RTL. *) + +Inductive stackframe : Type := + Stackframe : + forall (res : reg) + (m : module) + (pc : node) + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), + stackframe. + +Inductive state : Type := +| State : + forall (stack : list stackframe) + (m : module) + (st : node) + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), state +| Returnstate : + forall (res : list stackframe) + (v : value), state +| Callstate : + forall (stack : list stackframe) + (m : module) + (args : list value), state. + +Definition binop_run (op : binop) (v1 v2 : value) : option value := + match op with + | Vadd => Some (Int.add v1 v2) + | Vsub => Some (Int.sub v1 v2) + | Vmul => Some (Int.mul v1 v2) + | Vdiv => if Int.eq v2 Int.zero + || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone + then None + else Some (Int.divs v1 v2) + | Vdivu => if Int.eq v2 Int.zero then None else Some (Int.divu v1 v2) + | Vmod => if Int.eq v2 Int.zero + || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone + then None + else Some (Int.mods v1 v2) + | Vmodu => if Int.eq v2 Int.zero then None else Some (Int.modu v1 v2) + | Vlt => Some (boolToValue (Int.lt v1 v2)) + | Vltu => Some (boolToValue (Int.ltu v1 v2)) + | Vgt => Some (boolToValue (Int.lt v2 v1)) + | Vgtu => Some (boolToValue (Int.ltu v2 v1)) + | Vle => Some (boolToValue (negb (Int.lt v2 v1))) + | Vleu => Some (boolToValue (negb (Int.ltu v2 v1))) + | Vge => Some (boolToValue (negb (Int.lt v1 v2))) + | Vgeu => Some (boolToValue (negb (Int.ltu v1 v2))) + | Veq => Some (boolToValue (Int.eq v1 v2)) + | Vne => Some (boolToValue (negb (Int.eq v1 v2))) + | Vand => Some (Int.and v1 v2) + | Vor => Some (Int.or v1 v2) + | Vxor => Some (Int.xor v1 v2) + | Vshl => Some (Int.shl v1 v2) + | Vshr => Some (Int.shr v1 v2) + | Vshru => Some (Int.shru v1 v2) + end. + +Definition unop_run (op : unop) (v1 : value) : value := + match op with + | Vneg => Int.neg v1 + | Vnot => Int.not v1 + end. + +Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop := + | erun_Vlit : + forall fext reg stack v, + expr_runp fext reg stack (Vlit v) v + | erun_Vvar : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvar r) v + | erun_Vvari : + forall fext reg stack v iexp i r, + expr_runp fext reg stack iexp i -> + arr_assocmap_lookup stack r (valueToNat i) = Some v -> + expr_runp fext reg stack (Vvari r iexp) v + | erun_Vbinop : + forall fext reg stack op l r lv rv resv, + expr_runp fext reg stack l lv -> + expr_runp fext reg stack r rv -> + Some resv = binop_run op lv rv -> + expr_runp fext reg stack (Vbinop op l r) resv + | erun_Vunop : + forall fext reg stack u vu op oper resv, + expr_runp fext reg stack u vu -> + oper = unop_run op -> + resv = oper vu -> + expr_runp fext reg stack (Vunop op u) resv + | erun_Vternary_true : + forall fext reg stack c ts fs vc vt, + expr_runp fext reg stack c vc -> + expr_runp fext reg stack ts vt -> + valueToBool vc = true -> + expr_runp fext reg stack (Vternary c ts fs) vt + | erun_Vternary_false : + forall fext reg stack c ts fs vc vf, + expr_runp fext reg stack c vc -> + expr_runp fext reg stack fs vf -> + valueToBool vc = false -> + expr_runp fext reg stack (Vternary c ts fs) vf. +Hint Constructors expr_runp : verilog. + +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. + +(*Definition access_fext (f : fext) (r : reg) : res value := + match AssocMap.get r f with + | Some v => OK v + | _ => OK (ZToValue 0) + end.*) + +(* TODO FIX Vvar case without default *) +(*Fixpoint expr_run (assoc : assocmap) (e : expr) + {struct e} : res value := + match e with + | Vlit v => OK v + | Vvar r => match s with + | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r + | _ => Error (msg "Verilog: Wrong state") + end + | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled") + | Vinputvar r => access_fext s r + | Vbinop op l r => + let lv := expr_run s l in + let rv := expr_run s 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 s e; + OK (oper ev) + | Vternary c te fe => + do cv <- expr_run s c; + if valueToBool cv then expr_run s te else expr_run s fe + end.*) + +(** Return the location of the lhs of an assignment. *) + +Inductive location : Type := +| LocReg (_ : reg) +| LocArray (_ : reg) (_ : nat). + +Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop := +| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r) +| Indexed : forall f asr asa r iexp iv, + expr_runp f asr asa iexp iv -> + location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)). + +(* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l) (e : expr) : res reg := *) +(* match e with *) +(* | Vvar r => OK r *) +(* | _ => Error (msg "Verilog: expression not supported on lhs of assignment") *) +(* end. *) + +(*Fixpoint stmnt_height (st : stmnt) {struct st} : nat := + match st with + | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2) + | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2)) + | Vcase _ ls (Some st) => + S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls) + | _ => 1 + end. + +Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt)) + {struct cl} : option (res stmnt) := + match cl with + | (e, st)::xs => + match expr_run s e with + | OK v' => + match eq_to_opt v v' (veq v v') with + | Some eq => if valueToBool eq then Some (OK st) else find_case_stmnt s v xs + | None => Some (Error (msg "Verilog: equality check sizes not equal")) + end + | Error msg => Some (Error msg) + end + | _ => None + end. + +Fixpoint stmnt_run' (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' n' s s1; + stmnt_run' n' s' s2 + | Vcond c st sf => + do cv <- expr_run s c; + if valueToBool cv + then stmnt_run' n' s st + else stmnt_run' n' s sf + | Vcase e cl defst => + do v <- expr_run s e; + match find_case_stmnt s v cl with + | Some (OK st') => stmnt_run' n' s st' + | Some (Error msg) => Error msg + | None => do s' <- handle_opt (msg "Verilog: no case was matched") + (option_map (stmnt_run' n' s) defst); s' + end + | Vblock lhs rhs => + match s with + | State m assoc nbassoc f c => + do name <- assign_name lhs; + do rhse <- expr_run s rhs; + OK (State m (PositiveMap.add name rhse assoc) nbassoc f c) + | _ => Error (msg "Verilog: Wrong state") + end + | Vnonblock lhs rhs => + match s with + | State m assoc nbassoc f c => + do name <- assign_name lhs; + do rhse <- expr_run s rhs; + OK (State m assoc (PositiveMap.add name rhse nbassoc) f c) + | _ => Error (msg "Verilog: Wrong state") + end + end + | _ => OK s + end. + +Definition stmnt_run (s : state) (st : stmnt) : res state := + stmnt_run' (stmnt_height st) s st. *) + +Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> + stmnt -> reg_associations -> arr_associations -> Prop := +| stmnt_runp_Vskip: + forall f ar al, stmnt_runp f ar al Vskip ar al +| stmnt_runp_Vseq: + forall f st1 st2 asr0 asa0 asr1 asa1 asr2 asa2, + stmnt_runp f asr0 asa0 st1 asr1 asa1 -> + stmnt_runp f asr1 asa1 st2 asr2 asa2 -> + stmnt_runp f asr0 asa0 (Vseq st1 st2) asr2 asa2 +| stmnt_runp_Vcond_true: + forall asr0 asa0 asr1 asa1 f c vc stt stf, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc -> + valueToBool vc = true -> + stmnt_runp f asr0 asa0 stt asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1 +| stmnt_runp_Vcond_false: + forall asr0 asa0 asr1 asa1 f c vc stt stf, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc -> + valueToBool vc = false -> + stmnt_runp f asr0 asa0 stf asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1 +| stmnt_runp_Vcase_nomatch: + forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> + mve <> ve -> + stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 +| stmnt_runp_Vcase_match: + forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> + mve = ve -> + stmnt_runp f asr0 asa0 sc asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 +| stmnt_runp_Vcase_default: + forall asr0 asa0 asr1 asa1 f st e ve, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> + stmnt_runp f asr0 asa0 st asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1 +| stmnt_runp_Vblock_reg: + forall lhs r rhs rhsval asr asa f, + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> + expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> + stmnt_runp f asr asa + (Vblock lhs rhs) + (block_reg r asr rhsval) asa +| stmnt_runp_Vnonblock_reg: + forall lhs r rhs rhsval asr asa f, + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> + expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> + stmnt_runp f asr asa + (Vnonblock lhs rhs) + (nonblock_reg r asr rhsval) asa +| stmnt_runp_Vblock_arr: + forall lhs r i rhs rhsval asr asa f, + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> + expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> + stmnt_runp f asr asa + (Vblock lhs rhs) + asr (block_arr r i asa rhsval) +| stmnt_runp_Vnonblock_arr: + forall lhs r i rhs rhsval asr asa f, + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> + expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> + stmnt_runp f asr asa + (Vnonblock lhs rhs) + asr (nonblock_arr r i asa rhsval). +Hint Constructors stmnt_runp : verilog. + +(*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := + let run := fun st ls => + do s' <- stmnt_run s st; + mi_step 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 s ls + | (Vdeclarr _ _ _)::ls => mi_step s ls + | nil => OK s + end.*) + +Inductive mi_stepp : fext -> reg_associations -> arr_associations -> + module_item -> reg_associations -> arr_associations -> Prop := +| mi_stepp_Valways : + forall f sr0 sa0 st sr1 sa1 c, + stmnt_runp f sr0 sa0 st sr1 sa1 -> + mi_stepp f sr0 sa0 (Valways c st) sr1 sa1 +| mi_stepp_Valways_ff : + forall f sr0 sa0 st sr1 sa1 c, + stmnt_runp f sr0 sa0 st sr1 sa1 -> + mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1 +| mi_stepp_Valways_comb : + forall f sr0 sa0 st sr1 sa1 c, + stmnt_runp f sr0 sa0 st sr1 sa1 -> + mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1 +| mi_stepp_Vdecl : + forall f sr sa d, + mi_stepp f sr sa (Vdeclaration d) sr sa. +Hint Constructors mi_stepp : verilog. + +Inductive mis_stepp : fext -> reg_associations -> arr_associations -> + list module_item -> reg_associations -> arr_associations -> Prop := +| mis_stepp_Cons : + forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2, + mi_stepp f sr0 sa0 mi sr1 sa1 -> + mis_stepp f sr1 sa1 mis sr2 sa2 -> + mis_stepp f sr0 sa0 (mi :: mis) sr2 sa2 +| mis_stepp_Nil : + forall f sr sa, + mis_stepp f sr sa nil sr sa. +Hint Constructors mis_stepp : verilog. + +(*Definition mi_step_commit (s : state) (m : list module_item) : res state := + match mi_step s m with + | OK (State m assoc nbassoc f c) => + OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c) + | Error msg => Error msg + | _ => Error (msg "Verilog: Wrong state") + end. + +Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat) + {struct n} : res assocmap := + match n with + | S n' => + do assoc' <- mi_run f assoc m n'; + match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with + | OK (State assoc _ _ _) => OK assoc + | Error m => Error m + end + | O => OK assoc + end.*) + +(** Resets the module into a known state, so that it can be executed. This is +assumed to be the starting state of the module, and may have to be changed if +other arguments to the module are also to be supported. *) + +(*Definition initial_fextclk (m : module) : fextclk := + fun x => match x with + | S O => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap) + | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap) + end.*) + +(*Definition module_run (n : nat) (m : module) : res assocmap := + mi_run (initial_fextclk m) empty_assocmap (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. + + *) + +Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := + match rl, vl with + | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl') + | _, _ => empty_assocmap + end. + +Definition genv := Globalenvs.Genv.t fundef unit. +Definition empty_stack (m : module) : assocmap_arr := + (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)). + +Inductive step : genv -> state -> Events.trace -> state -> Prop := + | step_module : + forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist, + asr!(m.(mod_reset)) = Some (ZToValue 0) -> + asr!(m.(mod_finish)) = Some (ZToValue 0) -> + asr!(m.(mod_st)) = Some ist -> + valueToPos ist = st -> + mis_stepp f (mkassociations asr empty_assocmap) + (mkassociations asa (empty_stack m)) + m.(mod_body) + (mkassociations basr1 nasr1) + (mkassociations basa1 nasa1)-> + asr' = merge_regs nasr1 basr1 -> + asa' = merge_arrs nasa1 basa1 -> + asr'!(m.(mod_st)) = Some stval -> + valueToPos stval = pstval -> + step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') +| step_finish : + forall asr asa sf retval m st g, + asr!(m.(mod_finish)) = Some (ZToValue 1) -> + asr!(m.(mod_return)) = Some retval -> + step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) +| step_call : + forall g res m args, + step g (Callstate res m args) Events.E0 + (State res m m.(mod_entrypoint) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint)) + (init_params args m.(mod_args))))) + (empty_stack m)) +| step_return : + forall g m asr i r sf pc mst asa, + mst = mod_st m -> + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). +Hint Constructors step : verilog. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b m0 m, + let ge := Globalenvs.Genv.globalenv p in + Globalenvs.Genv.init_mem p = Some m0 -> + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> + initial_state p (Callstate nil m nil). + +Inductive final_state : state -> Integers.int -> Prop := +| final_state_intro : forall retval retvali, + retvali = valueToInt retval -> + final_state (Returnstate nil retval) retvali. + +Definition semantics (m : program) := + Smallstep.Semantics step (initial_state m) final_state + (Globalenvs.Genv.globalenv m). + +Lemma expr_runp_determinate : + forall f e asr asa v, + expr_runp f asr asa e v -> + forall v', + expr_runp f asr asa e v' -> + v' = v. +Proof. + induction e; intros; + + repeat (try match goal with + | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H + + | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _, + H2 : expr_runp _ _ _ ?e _ |- _ ] => + learn (H1 _ _ _ H2) + | [ H1 : forall v, expr_runp _ ?asr ?asa ?e v -> _, + H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => + learn (H1 _ H2) + end; crush). +Qed. +Hint Resolve expr_runp_determinate : verilog. + +Lemma location_is_determinate : + forall f asr asa e l, + location_is f asr asa e l -> + forall l', + location_is f asr asa e l' -> + l' = l. +Proof. + induction 1; intros; + + repeat (try match goal with + | [ H : location_is _ _ _ _ _ |- _ ] => invert H + | [ H1 : expr_runp _ ?asr ?asa ?e _, + H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => + learn (expr_runp_determinate H1 H2) + end; crush). +Qed. + +Lemma stmnt_runp_determinate : + forall f s asr0 asa0 asr1 asa1, + stmnt_runp f asr0 asa0 s asr1 asa1 -> + forall asr1' asa1', + stmnt_runp f asr0 asa0 s asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. + induction 1; intros; + + repeat (try match goal with + | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcase _ (_ :: _) _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcase _ [] _) _ _ |- _ ] => invert H + + | [ H1 : expr_runp _ ?asr ?asa ?e _, + H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => + learn (expr_runp_determinate H1 H2) + + | [ H1 : location_is _ ?asr ?asa ?e _, + H2 : location_is _ ?asr ?asa ?e _ |- _ ] => + learn (location_is_determinate H1 H2) + + | [ H1 : forall asr1 asa1, stmnt_runp _ ?asr0 ?asa0 ?s asr1 asa1 -> _, + H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (H1 _ _ H2) + end; crush). +Qed. +Hint Resolve stmnt_runp_determinate : verilog. + +Lemma mi_stepp_determinate : + forall f asr0 asa0 m asr1 asa1, + mi_stepp f asr0 asa0 m asr1 asa1 -> + forall asr1' asa1', + mi_stepp f asr0 asa0 m asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. +Proof. + intros. destruct m; invert H; invert H0; + + repeat (try match goal with + | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _, + H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (stmnt_runp_determinate H1 H2) + end; crush). +Qed. + +Lemma mis_stepp_determinate : + forall f asr0 asa0 m asr1 asa1, + mis_stepp f asr0 asa0 m asr1 asa1 -> + forall asr1' asa1', + mis_stepp f asr0 asa0 m asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. +Proof. + induction 1; intros; + + repeat (try match goal with + | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => invert H + | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H + + | [ H1 : mi_stepp _ ?asr0 ?asa0 ?s _ _, + H2 : mi_stepp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (mi_stepp_determinate H1 H2) + + | [ H1 : forall asr1 asa1, mis_stepp _ ?asr0 ?asa0 ?m asr1 asa1 -> _, + H2 : mis_stepp _ ?asr0 ?asa0 ?m _ _ |- _ ] => + learn (H1 _ _ H2) + end; crush). +Qed. + +Lemma semantics_determinate : + forall (p: program), Smallstep.determinate (semantics p). +Proof. + intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. + - invert H; invert H0; constructor. (* Traces are always empty *) + - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. + pose proof (mis_stepp_determinate H5 H15). + crush. + - constructor. invert H; crush. + - invert H; invert H0; unfold ge0, ge1 in *; crush. + - red; simplify; intro; invert H0; invert H; crush. + - invert H; invert H0; crush. +Qed. |