diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:19 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:19 +0100 |
commit | b32e7574864cde80f8f5283431c21a6803a89108 (patch) | |
tree | f30babb0db7e5797cb77f6ac44a682cb9b8b105b /src/hls | |
parent | c321e39de166308d8db2f6ebe577edb3297b507c (diff) | |
download | vericert-b32e7574864cde80f8f5283431c21a6803a89108.tar.gz vericert-b32e7574864cde80f8f5283431c21a6803a89108.zip |
Fix backend hardware generation and scheduling
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/DHTL.v | 9 | ||||
-rw-r--r-- | src/hls/DMemorygen.v | 5 | ||||
-rw-r--r-- | src/hls/DVeriloggen.v | 21 | ||||
-rw-r--r-- | src/hls/HTLPargen.v | 18 | ||||
-rw-r--r-- | src/hls/PrintVerilog.ml | 17 | ||||
-rw-r--r-- | src/hls/Schedule.ml | 52 |
6 files changed, 80 insertions, 42 deletions
diff --git a/src/hls/DHTL.v b/src/hls/DHTL.v index b80123c..6be82ae 100644 --- a/src/hls/DHTL.v +++ b/src/hls/DHTL.v @@ -70,7 +70,7 @@ Record ram := mk_ram { /\ ram_wr_en < ram_u_en) }. -Definition module_ordering a b c d e f g := a < b < c /\ c < d < e /\ e < f < g. +Definition module_ordering a b c d e f g h := a < b < c /\ c < d < e /\ e < f < g /\ g < h. Record module: Type := mkmodule { @@ -85,12 +85,13 @@ Record module: Type := mod_start : reg; mod_reset : reg; mod_clk : reg; + mod_preg : 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_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_ordering_wf : module_ordering mod_st mod_finish mod_return mod_stk mod_start mod_reset mod_clk mod_preg; + mod_ram_wf : forall r', mod_ram = Some r' -> mod_preg < ram_addr r'; mod_params_wf : Forall (Pos.gt mod_st) mod_params; }. @@ -265,7 +266,7 @@ Definition max_reg_module 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 (mod_clk m) (Pos.max (mod_preg m) (max_reg_ram (mod_ram m))))))))))). Lemma max_fold_lt : forall m l n, m <= n -> m <= (fold_left Pos.max l n). diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v index 0ac0ff0..bef9f3d 100644 --- a/src/hls/DMemorygen.v +++ b/src/hls/DMemorygen.v @@ -298,7 +298,7 @@ Proof. lia. Qed. Lemma module_ram_wf' : forall m addr, addr = max_reg_module m + 1 -> - mod_clk m < addr. + mod_preg m < addr. Proof. unfold max_reg_module; lia. Qed. Definition transf_module (m: module): module. @@ -326,6 +326,7 @@ Definition transf_module (m: module): module. (mod_start m) (mod_reset m) (mod_clk m) + (mod_preg m) (AssocMap.set u_en (None, VScalar 1) (AssocMap.set en (None, VScalar 1) (AssocMap.set wr_en (None, VScalar 1) @@ -3374,7 +3375,7 @@ Section CORRECTNESS. { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } assert ((init_regs nil (mod_params m)) ! (ram_u_en r) = None). { apply init_regs_equal_empty. eapply forall_lt_num. eassumption. lia. } - unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H14. auto. + unfold find_assocmap, AssocMapExt.get_default. rewrite H7. rewrite H15. auto. - econstructor. econstructor. apply Smallstep.plus_one. econstructor. replace (mod_entrypoint (transf_module m)) with (mod_entrypoint m). replace (mod_reset (transf_module m)) with (mod_reset m). diff --git a/src/hls/DVeriloggen.v b/src/hls/DVeriloggen.v index 3f8a0b7..6b47dd0 100644 --- a/src/hls/DVeriloggen.v +++ b/src/hls/DVeriloggen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2023 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -55,15 +55,19 @@ Definition inst_ram clk ram := Definition transl_module (m : DHTL.module) : Verilog.module := let case_el_data := list_to_stmnt (transl_list (PTree.elements m.(mod_datapath))) in + (* let nstate := (max_reg_module m + 1)%positive in *) match m.(DHTL.mod_ram) with | Some ram => let body := - Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) + Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) (Vnonblock (Vvar m.(DHTL.mod_st)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) -(Vcase (Vvar m.(DHTL.mod_st)) case_el_data (Some Vskip))) +(Vcase (Vvar (DHTL.mod_st m)) case_el_data (Some Vskip))) + (* :: Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) *) + (* (Vnonblock (Vvar (DHTL.mod_st m)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) (Vnonblock (Vvar (DHTL.mod_st m)) (Vvar m.(DHTL.mod_st)))) *) :: inst_ram m.(DHTL.mod_clk) ram - :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) - ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in + :: List.map Vdeclaration ((* Vdecl None nstate 32 :: *) + (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) + ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls)))) in Verilog.mkmodule m.(DHTL.mod_start) m.(DHTL.mod_reset) m.(DHTL.mod_clk) @@ -79,8 +83,11 @@ Definition transl_module (m : DHTL.module) : Verilog.module := let body := Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) (Vnonblock (Vvar m.(DHTL.mod_st)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) -(Vcase (Vvar m.(DHTL.mod_st)) case_el_data (Some Vskip))) - :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) +(Vcase (Vvar (DHTL.mod_st m)) case_el_data (Some Vskip))) + (* :: Valways (Vposedge m.(DHTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(DHTL.mod_reset)) (Vlit (ZToValue 1))) *) + (* (Vnonblock (Vvar (DHTL.mod_st m)) (Vlit (posToValue m.(DHTL.mod_entrypoint)))) *) + (* (Vnonblock (Vvar (DHTL.mod_st m)) (Vvar m.(DHTL.mod_st)))) *) + :: List.map Vdeclaration ((* Vdecl None (DHTL.mod_st m) 32 :: *)arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in Verilog.mkmodule m.(DHTL.mod_start) m.(DHTL.mod_reset) diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index f22cc39..1bc0fd5 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -1,7 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2023 Yann Herklotz <yann@yannherklotz.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -570,9 +569,9 @@ Proof. simplify. transitivity (Z.pos (max_pc_map m)); eauto. Qed. -Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. +Definition decide_order a b c d e f g h : {module_ordering a b c d e f g h} + {True}. refine (match bool_dec ((a <? b) && (b <? c) && (c <? d) - && (d <? e) && (e <? f) && (f <? g))%positive true with + && (d <? e) && (e <? f) && (f <? g) && (g <? h))%positive true with | left t => left _ | _ => _ end); auto. @@ -586,17 +585,17 @@ Definition transf_module (f: function) : mon DHTL.module. if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; - do preg <- create_reg None 32; do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); - do _stmnt <- collectlist (transf_seq_blockM fin rtrn stack preg) (Maps.PTree.elements f.(GiblePar.fn_code)); - do _stmnt' <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(GiblePar.fn_params); - do _stmnt'' <- collectlist declare_all_regs (Maps.PTree.elements f.(GiblePar.fn_code)); do start <- create_reg (Some Vinput) 1; do rst <- create_reg (Some Vinput) 1; do clk <- create_reg (Some Vinput) 1; + do preg <- create_reg None 128; + do _stmnt <- collectlist (transf_seq_blockM fin rtrn stack preg) (Maps.PTree.elements f.(GiblePar.fn_code)); + do _stmnt' <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(GiblePar.fn_params); + do _stmnt'' <- collectlist declare_all_regs (Maps.PTree.elements f.(GiblePar.fn_code)); do current_state <- get; match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, - decide_order (st_st current_state) fin rtrn stack start rst clk, + decide_order (st_st current_state) fin rtrn stack start rst clk preg, max_list_dec (GiblePar.fn_params f) (st_st current_state) with | left LEDATA, left MORD, left WFPARAMS => @@ -612,6 +611,7 @@ Definition transf_module (f: function) : mon DHTL.module. start rst clk + preg current_state.(st_scldecls) current_state.(st_arrdecls) None diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index 46b001e..2e0f0e1 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -111,7 +111,7 @@ let rec pprint_stmnt i = indent (i + 1); "end\n" ] in function - | Vskip -> concat [indent i; ";\n"] + | Vskip -> "" | Vseq (s1, s2) -> concat [ pprint_stmnt i s1; pprint_stmnt i s2] | Vcond (e, st, sf) -> concat [ indent i; "if ("; pprint_expr e; ") begin\n"; pprint_stmnt (i + 1) st; indent i; "end else begin\n"; @@ -147,7 +147,7 @@ let declare (t, i) = let declarearr (t, _) = function (r, sz, ln) -> - concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; + concat [t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; register r; " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ] @@ -159,19 +159,20 @@ let print_io = function let decl i = function | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)] - | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)] + | Vdeclarr (io, r, sz, ln) -> concat [indent i; "(* ram_style = \"block\" *)\n"; + indent i; declarearr (print_io io) (r, sz, ln)] (* TODO Fix always blocks, as they currently always print the same. *) let pprint_module_item i = function | Vdeclaration d -> decl i d | Valways (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; " begin\n"; + concat ["\n"; indent i; "always "; pprint_edge_top i e; " begin\n"; pprint_stmnt (i+1) s; indent i; "end\n"] | Valways_ff (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; " begin\n"; + concat ["\n"; indent i; "always "; pprint_edge_top i e; " begin\n"; pprint_stmnt (i+1) s; indent i; "end\n"] | Valways_comb (e, s) -> - concat [indent i; "always "; pprint_edge_top i e; " begin\n"; + concat ["\n"; indent i; "always "; pprint_edge_top i e; " begin\n"; pprint_stmnt (i+1) s; indent i; "end\n"] let rec intersperse c = function @@ -197,7 +198,8 @@ let make_io i io r = concat [indent i; io; " "; register r; ";\n"] let compose f g x = g x |> f -let testbench = "module testbench; +let testbench = "`ifndef SYNTHESIS +module testbench; reg start, reset, clk; wire finish; wire [31:0] return_val; @@ -225,6 +227,7 @@ let testbench = "module testbench; cycles <= cycles + 1; end endmodule +`endif " let debug_always_verbose i clk state = concat [ diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 683dd29..248d0f8 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -263,9 +263,35 @@ let read_process command = let comb_delay = function | RBnop -> 1 + | RBop (Some _, op, _, _) -> + (match op with + | Omove -> 64 + | Ointconst _ -> 1 + | Olongconst _ -> 1 + | Ocast8signed -> 1 + | Ocast8unsigned -> 1 + | Ocast16signed -> 1 + | Ocast16unsigned -> 1 + | Oneg -> 1 + | Onot -> 1 + | Oor -> 64 + | Oorimm _ -> 64 + | Oand -> 64 + | Oandimm _ -> 64 + | Oxor -> 64 + | Oxorimm _ -> 33 + | Omul -> 64 + | Omulimm _ -> 64 + | Omulhs -> 64 + | Omulhu -> 64 + | Odiv -> 576 + | Odivu -> 576 + | Omod -> 576 + | Omodu -> 576 + | _ -> 64) | RBop (_, op, _, _) -> (match op with - | Omove -> 1 + | Omove -> 16 | Ointconst _ -> 1 | Olongconst _ -> 1 | Ocast8signed -> 1 @@ -274,27 +300,27 @@ let comb_delay = function | Ocast16unsigned -> 1 | Oneg -> 1 | Onot -> 1 - | Oor -> 1 - | Oorimm _ -> 1 - | Oand -> 1 - | Oandimm _ -> 1 - | Oxor -> 1 - | Oxorimm _ -> 1 - | Omul -> 64 - | Omulimm _ -> 64 - | Omulhs -> 64 - | Omulhu -> 64 + | Oor -> 16 + | Oorimm _ -> 16 + | Oand -> 16 + | Oandimm _ -> 4 + | Oxor -> 16 + | Oxorimm _ -> 4 + | Omul -> 56 + | Omulimm _ -> 56 + | Omulhs -> 56 + | Omulhu -> 56 | Odiv -> 576 | Odivu -> 576 | Omod -> 576 | Omodu -> 576 - | _ -> 1) + | _ -> 16) | RBexit _ -> 64 (** Because of the limiations of memory generation we add a large combinational delay for loads and stores. *) | RBload _ -> 64 | RBstore _ -> 64 - | _ -> 1 + | _ -> 8 let pipeline_stages = function | RBload _ -> 1 (* TODO: Set back to 2 when memory inferrence is fixed. *) |