diff options
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/HTL.v | 21 | ||||
| -rw-r--r-- | src/verilog/Value.v | 5 | ||||
| -rw-r--r-- | src/verilog/Verilog.v | 8 |
3 files changed, 24 insertions, 10 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index c07d672..c509248 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -46,6 +46,7 @@ Record module: Type := mod_entrypoint : node; mod_st : reg; mod_stk : reg; + mod_stk_len : nat; mod_finish : reg; mod_return : reg; mod_start : reg; @@ -65,6 +66,14 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := | _, _ => empty_assocmap end. +Fixpoint zeroes' (acc : list value) (n : nat) : list value := + match n with + | O => acc + | S n => zeroes' ((NToValue 32 0)::acc) n + end. + +Definition zeroes : nat -> list value := zeroes' nil. + (** * Operational Semantics *) Definition genv := Globalenvs.Genv.t fundef unit. @@ -74,7 +83,8 @@ Inductive stackframe : Type := forall (res : reg) (m : module) (pc : node) - (assoc : assocmap), + (reg_assoc : assocmap) + (arr_assoc : AssocMap.t (list value)), stackframe. Inductive state : Type := @@ -130,13 +140,12 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State res m m.(mod_entrypoint) (AssocMap.set (mod_st m) (posToValue 32 m.(mod_entrypoint)) (init_regs args m.(mod_params))) - (AssocMap.empty (list value))) + (AssocMap.set m.(mod_stk) (zeroes m.(mod_stk_len)) (AssocMap.empty (list value)))) | step_return : - forall g m asr i r sf pc mst, + forall g m asr asa i r sf pc mst, mst = mod_st m -> - step g (Returnstate (Stackframe r m pc asr :: sf) i) Events.E0 - (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) - (AssocMap.empty (list value))). + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue 32 pc)) # r <- i) asa). Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := diff --git a/src/verilog/Value.v b/src/verilog/Value.v index d527b15..b1ee353 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -296,6 +296,11 @@ Inductive val_value_lessdef: val -> value -> Prop := val_value_lessdef (Vint i) v' | lessdef_undef: forall v, val_value_lessdef Vundef v. +Inductive opt_val_value_lessdef: option val -> value -> Prop := +| opt_lessdef_some: + forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' +| opt_lessdef_none: forall v, opt_val_value_lessdef None v. + Lemma valueToZ_ZToValue : forall n z, (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index b4b2f00..8b83d49 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -56,10 +56,10 @@ Definition merge_associations {A : Type} (assoc : associations A) := mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking)) (AssocMap.empty A). -Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := +Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : value := match a ! r with - | None => None - | Some arr => nth_error arr i + | None => natToValue 32 0 + | Some arr => nth i arr (natToValue 32 0) end. Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A := @@ -324,7 +324,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop | 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 -> + arr_assocmap_lookup stack r (valueToNat i) = v -> expr_runp fext reg stack (Vvari r iexp) v | erun_Vinputvar : forall fext reg stack r v, |