diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:14:30 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-11-18 22:14:30 +0000 |
commit | 3c5bd88f22f744e4908afbc5a56e202dfa469360 (patch) | |
tree | 57ddb252b09bdc61665fcab97ff169acc9af23e7 /src/hls/HTL.v | |
parent | e6348c97faee39754efd13b69a70c54851e2a789 (diff) | |
download | vericert-3c5bd88f22f744e4908afbc5a56e202dfa469360.tar.gz vericert-3c5bd88f22f744e4908afbc5a56e202dfa469360.zip |
Fix compilation with new HTL language
Diffstat (limited to 'src/hls/HTL.v')
-rw-r--r-- | src/hls/HTL.v | 72 |
1 files changed, 41 insertions, 31 deletions
diff --git a/src/hls/HTL.v b/src/hls/HTL.v index f4552a5..551c66e 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -57,8 +57,6 @@ Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := In p0 (map fst (Maps.PTree.elements m)) -> (Z.pos p0 <= Integers.Int.max_unsigned)%Z. -Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g. - Record module: Type := mkmodule { mod_params : list reg; @@ -66,8 +64,6 @@ Record module: Type := mod_controllogic : controllogic; mod_entrypoint : node; mod_st : reg; - mod_stk : reg; - mod_stk_len : nat; mod_finish : reg; mod_return : reg; mod_start : reg; @@ -75,11 +71,7 @@ Record module: Type := mod_clk : reg; mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); - mod_ram : option ram; - mod_wf : map_well_formed mod_controllogic /\ map_well_formed mod_datapath; - mod_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk; - mod_ram_wf : forall r', mod_ram = Some r' -> mod_clk < ram_addr r'; - mod_params_wf : Forall (Pos.gt mod_st) mod_params; + mod_ram : ram; }. Definition fundef := AST.fundef module. @@ -93,7 +85,7 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := end. Definition empty_stack (m : module) : Verilog.assocmap_arr := - (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)). + (AssocMap.set m.(mod_ram).(ram_mem) (Array.arr_repeat None m.(mod_ram).(ram_size)) (AssocMap.empty Verilog.arr)). (** * Operational Semantics *) @@ -124,13 +116,13 @@ Inductive state : Type := (args : list value), state. Inductive exec_ram: - Verilog.reg_associations -> Verilog.arr_associations -> option ram -> + Verilog.reg_associations -> Verilog.arr_associations -> ram -> Verilog.reg_associations -> Verilog.arr_associations -> Prop := | exec_ram_Some_idle: forall ra ar r, Int.eq (Verilog.assoc_blocking ra)#(ram_en r, 32) (Verilog.assoc_blocking ra)#(ram_u_en r, 32) = true -> - exec_ram ra ar (Some r) ra ar + exec_ram ra ar r ra ar | exec_ram_Some_write: forall ra ar r d_in addr en wr_en u_en, Int.eq en u_en = false -> @@ -140,7 +132,7 @@ Inductive exec_ram: (Verilog.assoc_blocking ra)!(ram_wr_en r) = Some wr_en -> (Verilog.assoc_blocking ra)!(ram_d_in r) = Some d_in -> (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> - exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) ra u_en) + exec_ram ra ar r (Verilog.nonblock_reg (ram_en r) ra u_en) (Verilog.nonblock_arr (ram_mem r) (valueToNat addr) ar d_in) | exec_ram_Some_read: forall ra ar r addr v_d_out en u_en, @@ -151,11 +143,8 @@ Inductive exec_ram: (Verilog.assoc_blocking ra)!(ram_addr r) = Some addr -> Verilog.arr_assocmap_lookup (Verilog.assoc_blocking ar) (ram_mem r) (valueToNat addr) = Some v_d_out -> - exec_ram ra ar (Some r) (Verilog.nonblock_reg (ram_en r) - (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) u_en) ar -| exec_ram_None: - forall r a, - exec_ram r a None r a. + exec_ram ra ar r (Verilog.nonblock_reg (ram_en r) + (Verilog.nonblock_reg (ram_d_out r) ra v_d_out) u_en) ar. Inductive step : genv -> state -> Events.trace -> state -> Prop := | step_module : @@ -233,6 +222,10 @@ Definition semantics (m : program) := Smallstep.Semantics step (initial_state m) final_state (Globalenvs.Genv.globalenv m). +Definition all_module_regs m := + all_ram_regs (mod_ram m) ++ + (mod_st m::mod_finish m::mod_return m::mod_start m::mod_reset m::mod_clk m::nil). + Definition max_pc_function (m: module) := List.fold_left Pos.max (List.map fst (PTree.elements m.(mod_controllogic))) 1. @@ -253,17 +246,20 @@ Definition max_reg_ram r := (Pos.max (ram_d_out ram) (ram_u_en ram))))))) end. -Definition max_reg_module m := +Definition max_reg_body m := Pos.max (max_list (mod_params m)) - (Pos.max (max_stmnt_tree (mod_datapath m)) - (Pos.max (max_stmnt_tree (mod_controllogic m)) - (Pos.max (mod_st m) - (Pos.max (mod_stk m) - (Pos.max (mod_finish m) - (Pos.max (mod_return m) - (Pos.max (mod_start m) - (Pos.max (mod_reset m) - (Pos.max (mod_clk m) (max_reg_ram (mod_ram m))))))))))). + (Pos.max (max_stmnt_tree (mod_datapath m)) + (max_stmnt_tree (mod_controllogic m))). + +Definition max_reg_module m := + Pos.max (max_reg_body m) (max_list (all_module_regs m)). + +Record wf_htl_module m := + mk_wf_htl_module { + mod_wf : map_well_formed (mod_controllogic m) /\ map_well_formed (mod_datapath m); + mod_ordering_wf : list_norepet (all_module_regs m); + mod_gt : Forall (Pos.lt (max_reg_body m)) (all_module_regs m); + }. Lemma max_fold_lt : forall m l n, m <= n -> m <= (fold_left Pos.max l n). @@ -320,12 +316,16 @@ Proof. intros. apply max_reg_stmnt_le_stmnt_tree in H; lia. Qed. Lemma max_stmnt_lt_module : forall m d i, + wf_htl_module m -> (mod_controllogic m) ! i = Some d \/ (mod_datapath m) ! i = Some d -> Verilog.max_reg_stmnt d < max_reg_module m + 1. Proof. - inversion 1 as [ Hv | Hv ]; unfold max_reg_module; - apply max_reg_stmnt_le_stmnt_tree in Hv; lia. -Qed. + intros. apply mod_gt in H. + unfold Pos.lt, max_reg_body, max_reg_module, max_list, all_module_regs, all_ram_regs in *. + simplify. + repeat match goal with H: Forall _ _ |- _ => inv H end. + inversion H0 as [Hv | Hv]; apply max_reg_stmnt_le_stmnt_tree in Hv. + Admitted. Lemma max_list_correct l st : st > max_list l -> Forall (Pos.gt st) l. Proof. induction l; crush; constructor; [|apply IHl]; lia. Qed. @@ -339,3 +339,13 @@ Definition max_list_dec (l: list reg) (st: reg) : {Forall (Pos.gt st) l} + {True ); auto. apply max_list_correct. apply Pos.ltb_lt in e. lia. Qed. + +Variant wf_htl_fundef: fundef -> Prop := + | wf_htl_fundef_external: forall ef, + wf_htl_fundef (AST.External ef) + | wf_htl_function_internal: forall f, + wf_htl_module f -> + wf_htl_fundef (AST.Internal f). + +Definition wf_htl_program (p: program) : Prop := + forall f id, In (id, AST.Gfun f) (AST.prog_defs p) -> wf_htl_fundef f. |