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 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'src/translation') 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 := -- cgit