Concatenation style loads.

3 files changed, 54 insertions, 49 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 35203f8..d1c1363 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -427,17 +427,13 @@ Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) :=
            (enumerate 0 ns).
 
 Definition create_single_cycle_load (stack : reg) (addr : expr) (dst : reg) : stmnt :=
-  let l0   := Vnonblock (Vvarb0 dst) (Vvari stack addr) in
-  let l1   := Vnonblock (Vvarb1 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) in
-  let l2   := Vnonblock (Vvarb2 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) in
-  let l3   := Vnonblock (Vvarb3 dst) (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2))
-  in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3.
+  Vnonblock (Vvar dst) (Vload stack addr).
 
 Definition create_single_cycle_store (stack : reg) (addr : expr) (src : reg) : stmnt :=
   let l0   := Vnonblock (Vvari stack addr) (Vvarb0 src) in
   let l1   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 1)) (Vvarb1 src) in
   let l2   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb2 src) in
-  let l3   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 2)) (Vvarb3 src)
+  let l3   := Vnonblock (Vvari stack $ Vbinop Vadd addr (Vlit $ ZToValue 3)) (Vvarb3 src)
   in Vseq l0 $ Vseq l1 $ Vseq l2 $ l3.
 
 Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit :=
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index db78ad5..7f3eb29 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -72,9 +72,16 @@ let register a = sprintf "reg_%d" (P.to_int a)
 
 let literal l = sprintf "32'd%d" (Z.to_int (uvalueToZ l))
 
+let literal_int i = sprintf "32'd%d" i
+
 let byte n s = sprintf "reg_%d[%d:%d]" (P.to_int s) (7 + n * 8) (n * 8)
 
-let rec pprint_expr = function
+
+let rec pprint_expr =
+  let array_byte r i = function
+     | 0 -> concat [register r; "["; pprint_expr i; "]"]
+     | n -> concat [register r; "["; pprint_expr i; " + "; literal_int n; "][7:0]"]
+  in function
   | Vlit l -> literal l
   | Vvar s -> register s
   | Vvarb0 s -> byte 0 s
@@ -86,6 +93,7 @@ let rec pprint_expr = function
   | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
   | 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; ")"]
+  | Vload (s, i) -> concat ["{"; array_byte s i 3; ", "; array_byte s i 2; ", "; array_byte s i 1; ", "; array_byte s i 0; "}"]
 
 let rec pprint_stmnt i =
   let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s;
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 108ac72..94e6184 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -164,7 +164,8 @@ Inductive expr : Type :=
 | Vinputvar : reg -> expr
 | Vbinop : binop -> expr -> expr -> expr
 | Vunop : unop -> expr -> expr
-| Vternary : expr -> expr -> expr -> expr.
+| Vternary : expr -> expr -> expr -> expr
+| Vload : reg -> expr -> expr.    (** 4-byte concatenation load *)
 
 Definition posToExpr (p : positive) : expr :=
   Vlit (posToValue p).
@@ -338,61 +339,61 @@ Definition unop_run (op : unop) (v1 : value) : value :=
 
 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
+      forall fext asr asa v,
+      expr_runp fext asr asa (Vlit v) v
   | erun_Vvar :
-      forall fext reg stack v r,
-      reg#r = v ->
-      expr_runp fext reg stack (Vvar r) v
+      forall fext asr asa v r,
+      asr#r = v ->
+      expr_runp fext asr asa (Vvar r) v
   | erun_Vvarb0 :
-      forall fext reg stack v r,
-      reg#r = v ->
-      expr_runp fext reg stack (Vvarb0 r) (IntExtra.ibyte0 v)
+      forall fext asr asa v r,
+      asr#r = v ->
+      expr_runp fext asr asa (Vvarb0 r) (IntExtra.ibyte0 v)
   | erun_Vvarb1 :
-      forall fext reg stack v r,
-      reg#r = v ->
-      expr_runp fext reg stack (Vvarb1 r) (IntExtra.ibyte1 v)
+      forall fext asr asa v r,
+      asr#r = v ->
+      expr_runp fext asr asa (Vvarb1 r) (IntExtra.ibyte1 v)
   | erun_Vvarb2 :
-      forall fext reg stack v r,
-      reg#r = v ->
-      expr_runp fext reg stack (Vvarb2 r) (IntExtra.ibyte2 v)
+      forall fext asr asa v r,
+      asr#r = v ->
+      expr_runp fext asr asa (Vvarb2 r) (IntExtra.ibyte2 v)
   | erun_Vvarb3 :
-      forall fext reg stack v r,
-      reg#r = v ->
-      expr_runp fext reg stack (Vvarb3 r) (IntExtra.ibyte3 v)
+      forall fext asr asa v r,
+      asr#r = v ->
+      expr_runp fext asr asa (Vvarb3 r) (IntExtra.ibyte3 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
+      forall fext asr asa v iexp i r,
+      expr_runp fext asr asa iexp i ->
+      arr_assocmap_lookup asa r (valueToNat i) = Some v ->
+      expr_runp fext asr asa (Vvari r iexp) v
   | erun_Vinputvar :
-      forall fext reg stack r v,
+      forall fext asr asa r v,
       fext!r = Some v ->
-      expr_runp fext reg stack (Vinputvar r) v
+      expr_runp fext asr asa (Vinputvar r) 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 ->
+      forall fext asr asa op l r lv rv resv,
+      expr_runp fext asr asa l lv ->
+      expr_runp fext asr asa r rv ->
       Some resv = binop_run op lv rv ->
-      expr_runp fext reg stack (Vbinop op l r) resv
+      expr_runp fext asr asa (Vbinop op l r) resv
   | erun_Vunop :
-      forall fext reg stack u vu op oper resv,
-      expr_runp fext reg stack u vu ->
+      forall fext asr asa u vu op oper resv,
+      expr_runp fext asr asa u vu ->
       oper = unop_run op ->
       resv = oper vu ->
-      expr_runp fext reg stack (Vunop op u) resv
+      expr_runp fext asr asa (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 ->
+      forall fext asr asa c ts fs vc vt,
+      expr_runp fext asr asa c vc ->
+      expr_runp fext asr asa ts vt ->
       valueToBool vc = true ->
-      expr_runp fext reg stack (Vternary c ts fs) vt
+      expr_runp fext asr asa (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 ->
+      forall fext asr asa c ts fs vc vf,
+      expr_runp fext asr asa c vc ->
+      expr_runp fext asr asa fs vf ->
       valueToBool vc = false ->
-      expr_runp fext reg stack (Vternary c ts fs) vf.
+      expr_runp fext asr asa (Vternary c ts fs) vf.
 Hint Constructors expr_runp : verilog.
 
 Definition handle_opt {A : Type} (err : errmsg) (val : option A)
@@ -449,12 +450,11 @@ Definition access_fext (f : fext) (r : reg) : res value :=
 
 Inductive location : Type :=
 | LocReg (_ : reg)
-| LocRegB (_ : reg) (_ : nat)
 | 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,
+| Reg : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r)
+| RegIndexed : 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)).
 
@@ -807,6 +807,7 @@ Proof.
               | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vload _ _) _ |- _ ] => invert H
 
               | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _,
                   H2 : expr_runp _ _ _ ?e _ |- _ ] =>