From 975a5fb0c11af6e8db3f250322794c0712f4af90 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 1 Mar 2021 11:05:12 +0000 Subject: Change lists in case statements to stmnt_list --- src/extraction/Extraction.v | 1 + src/hls/HTLPargen.v | 2 +- src/hls/PrintVerilog.ml | 4 +++- src/hls/Verilog.v | 29 ++++++++++++++++++++++------- src/hls/Veriloggen.v | 4 ++-- src/hls/Veriloggenproof.v | 2 +- 6 files changed, 30 insertions(+), 12 deletions(-) diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 8aec96e..7d6e57c 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -190,6 +190,7 @@ Separate Extraction HTLgen.tbl_to_case_expr Pipeline.pipeline RTLBlockInstr.sat_pred_temp + Verilog.stmnt_to_list Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 9213514..618c5e6 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -758,7 +758,7 @@ Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c)) | RBjumptable r tbl => do s <- get; - ret (Vskip, Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip)) + ret (Vskip, Vcase (Vvar r) (list_to_stmnt (tbl_to_case_expr s.(st_st) tbl)) (Some Vskip)) | RBcall sig ri rl r n => error (Errors.msg "HTLPargen: RPcall not supported.") | RBtailcall sig ri lr => diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index aeaf75c..3817fd3 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -118,7 +118,9 @@ let rec pprint_stmnt i = indent i; "end\n" ] | Vcase (e, es, d) -> concat [ indent i; "case ("; pprint_expr e; ")\n"; - fold_map pprint_case (List.sort compare_expr es |> List.rev); + fold_map pprint_case (stmnt_to_list es + |> List.sort compare_expr + |> List.rev); indent (i+1); "default:;\n"; indent i; "endcase\n" ] diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index a7db3ba..8e14267 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -174,9 +174,12 @@ Inductive stmnt : Type := | Vskip : stmnt | Vseq : stmnt -> stmnt -> stmnt | Vcond : expr -> stmnt -> stmnt -> stmnt -| Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt +| Vcase : expr -> stmnt_expr_list -> option stmnt -> stmnt | Vblock : expr -> expr -> stmnt -| Vnonblock : expr -> expr -> stmnt. +| Vnonblock : expr -> expr -> stmnt +with stmnt_expr_list : Type := +| Stmntnil : stmnt_expr_list +| Stmntcons : expr -> stmnt -> stmnt_expr_list -> stmnt_expr_list. (** ** Edges @@ -537,19 +540,19 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> mve <> ve -> stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 -> - stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 + stmnt_runp f asr0 asa0 (Vcase e (Stmntcons me sc cs) def) asr1 asa1 | stmnt_runp_Vcase_match: forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def, expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> mve = ve -> stmnt_runp f asr0 asa0 sc asr1 asa1 -> - stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 + stmnt_runp f asr0 asa0 (Vcase e (Stmntcons me sc cs) def) asr1 asa1 | stmnt_runp_Vcase_default: forall asr0 asa0 asr1 asa1 f st e ve, expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> stmnt_runp f asr0 asa0 st asr1 asa1 -> - stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1 + stmnt_runp f asr0 asa0 (Vcase e Stmntnil (Some st)) asr1 asa1 | stmnt_runp_Vblock_reg: forall lhs r rhs rhsval asr asa f, location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> @@ -764,6 +767,18 @@ Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). +Fixpoint list_to_stmnt st := + match st with + | (e, s) :: r => Stmntcons e s (list_to_stmnt r) + | nil => Stmntnil + end. + +Fixpoint stmnt_to_list st := + match st with + | Stmntcons e s r => (e, s) :: stmnt_to_list r + | Stmntnil => nil + end. + Lemma expr_runp_determinate : forall f e asr asa v, expr_runp f asr asa e v -> @@ -824,8 +839,8 @@ Lemma stmnt_runp_determinate : | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vcase _ (_ :: _) _) _ _ |- _ ] => invert H - | [ H : stmnt_runp _ _ _ (Vcase _ [] _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcase _ (Stmntcons _ _ _) _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcase _ Stmntnil _) _ _ |- _ ] => invert H | [ H1 : expr_runp _ ?asr ?asa ?e _, H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index 80c0669..894d309 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -43,8 +43,8 @@ Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. Definition transl_module (m : HTL.module) : Verilog.module := - let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in - let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in + let case_el_ctrl := list_to_stmnt (transl_list (PTree.elements m.(mod_controllogic))) in + let case_el_data := list_to_stmnt (transl_list (PTree.elements m.(mod_datapath))) in let body := Valways (Vposedge m.(HTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(HTL.mod_reset)) (Vlit (ZToValue 1))) (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint)))) diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 9abbd4b..99828e4 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -178,7 +178,7 @@ Lemma transl_list_correct : stmnt_runp f {| assoc_blocking := asr; assoc_nonblocking := asrn |} {| assoc_blocking := asa; assoc_nonblocking := asan |} - (Vcase (Vvar ev) (transl_list l) (Some Vskip)) + (Vcase (Vvar ev) (list_to_stmnt (transl_list l)) (Some Vskip)) {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). Proof. -- cgit