4 files changed, 40 insertions, 9 deletions

diff --git a/src/verilog/PrintHTL.ml b/src/verilog/PrintHTL.ml
index 0bdba51..36fdd3c 100644
--- a/src/verilog/PrintHTL.ml
+++ b/src/verilog/PrintHTL.ml
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-open Value
+open ValueInt
 open Datatypes
 open Camlcoq
 open AST
diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index 5265c97..db78ad5 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -17,7 +17,7 @@
  *)
 
 open Verilog
-open Value
+open ValueInt
 open Datatypes
 
 open Camlcoq
@@ -70,11 +70,17 @@ 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 (uvalueToZ l))
+let literal l = sprintf "32'd%d" (Z.to_int (uvalueToZ l))
+
+let byte n s = sprintf "reg_%d[%d:%d]" (P.to_int s) (7 + n * 8) (n * 8)
 
 let rec pprint_expr = function
   | Vlit l -> literal l
   | Vvar s -> register s
+  | Vvarb0 s -> byte 0 s
+  | Vvarb1 s -> byte 1 s
+  | Vvarb2 s -> byte 2 s
+  | Vvarb3 s -> byte 3 s
   | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"]
   | Vinputvar s -> register s
   | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"]
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index 62bf63f..5fd8fe9 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -18,8 +18,8 @@
 
 val pprint_stmnt : int -> Verilog.stmnt -> string
 
-val print_value : out_channel -> Value.value -> unit
+val print_value : out_channel -> ValueInt.value -> unit
 
 val print_program : bool -> out_channel -> Verilog.program -> unit
 
-val print_result : out_channel -> (BinNums.positive * Value.value) list -> unit
+val print_result : out_channel -> (BinNums.positive * ValueInt.value) list -> unit
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 064474a..921d9fd 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -29,7 +29,7 @@ Require Import Lia.
 
 Import ListNotations.
 
-From coqup Require Import common.Coquplib common.Show verilog.ValueInt AssocMap Array.
+From coqup Require Import common.Coquplib common.Show verilog.ValueInt IntegerExtra AssocMap Array.
 From compcert Require Events.
 From compcert Require Import Integers Errors Smallstep Globalenvs.
 
@@ -154,9 +154,13 @@ Inductive unop : Type :=
 (** ** Expressions *)
 
 Inductive expr : Type :=
-| Vlit : value -> expr
-| Vvar : reg -> expr
-| Vvari : reg -> expr -> expr
+| Vlit : value -> expr                    (** literal *)
+| Vvar : reg -> expr                      (** reg *)
+| Vvarb0 : reg -> expr                    (** 1st byte projection of reg *)
+| Vvarb1 : reg -> expr
+| Vvarb2 : reg -> expr
+| Vvarb3 : reg -> expr
+| Vvari : reg -> expr -> expr              (** array *)
 | Vinputvar : reg -> expr
 | Vbinop : binop -> expr -> expr -> expr
 | Vunop : unop -> expr -> expr
@@ -340,6 +344,22 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop
       forall fext reg stack v r,
       reg#r = v ->
       expr_runp fext reg stack (Vvar r) v
+  | erun_Vvarb0 :
+      forall fext reg stack v r,
+      reg#r = v ->
+      expr_runp fext reg stack (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)
+  | erun_Vvarb2 :
+      forall fext reg stack v r,
+      reg#r = v ->
+      expr_runp fext reg stack (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)
   | erun_Vvari :
       forall fext reg stack v iexp i r,
       expr_runp fext reg stack iexp i ->
@@ -429,6 +449,7 @@ 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 :=
@@ -775,6 +796,10 @@ Proof.
   repeat (try match goal with
               | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vvarb0 _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vvarb1 _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vvarb2 _) _ |- _ ] => invert H
+              | [ H : expr_runp _ _ _ (Vvarb3 _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H
               | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H