From ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 30 Aug 2020 14:03:40 +0100 Subject: Add RTLBlock intermediate language --- src/verilog/Verilog.v | 893 -------------------------------------------------- 1 file changed, 893 deletions(-) delete mode 100644 src/verilog/Verilog.v (limited to 'src/verilog/Verilog.v') diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v deleted file mode 100644 index 3b0dd0a..0000000 --- a/src/verilog/Verilog.v +++ /dev/null @@ -1,893 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * 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 . - *) - -From Coq Require Import - Structures.OrderedTypeEx - FSets.FMapPositive - Program.Basics - PeanoNat - ZArith - Lists.List - Program. - -Require Import Lia. - -Import ListNotations. - -From vericert Require Import common.Vericertlib common.Show verilog.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. -- cgit