From 897b2b15a810e996895dda0d863dcefb27dfabaf Mon Sep 17 00:00:00 2001 From: James Pollard Date: Mon, 6 Jul 2020 23:20:00 +0100 Subject: Concatenation style loads. --- src/translation/HTLgen.v | 8 ++--- src/verilog/PrintVerilog.ml | 10 +++++- src/verilog/Verilog.v | 85 +++++++++++++++++++++++---------------------- 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 _ |- _ ] => -- cgit