diff options
-rw-r--r-- | driver/VericertDriver.ml | 3 | ||||
-rw-r--r-- | src/Compiler.v | 2 | ||||
-rw-r--r-- | src/VericertClflags.ml | 1 | ||||
-rw-r--r-- | src/extraction/Extraction.v | 1 | ||||
-rw-r--r-- | src/hls/HTLPargen.v | 58 | ||||
-rw-r--r-- | src/hls/RTLParFUgen.v | 2 | ||||
-rw-r--r-- | src/hls/Schedule.ml | 9 |
7 files changed, 30 insertions, 46 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 467ae37..e89ff86 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -67,6 +67,7 @@ let compile_c_file sourcename ifile ofile = set_dest Vericert.PrintRTL.destination option_drtl ".rtl"; set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock"; set_dest Vericert.PrintRTLPar.destination option_drtlpar ".rtlpar"; + set_dest Vericert.PrintRTLParFU.destination option_drtlparfu ".rtlparfu"; set_dest Vericert.PrintHTL.destination option_dhtl ".htl"; set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Vericert.PrintLTL.destination option_dltl ".ltl"; @@ -393,6 +394,7 @@ let cmdline_actions = Exact "-drtl", Set option_drtl; Exact "-drtlblock", Set option_drtlblock; Exact "-drtlpar", Set option_drtlpar; + Exact "-drtlparfu", Set option_drtlparfu; Exact "-dhtl", Set option_dhtl; Exact "-dltl", Set option_dltl; Exact "-dalloctrace", Set option_dalloctrace; @@ -407,6 +409,7 @@ let cmdline_actions = option_drtl := true; option_drtlblock := true; option_drtlpar := true; + option_drtlparfu := true; option_dhtl := true; option_dltl := true; option_dalloctrace := true; diff --git a/src/Compiler.v b/src/Compiler.v index ff0938e..0ac2b80 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -86,6 +86,7 @@ Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: Z -> HTL.program -> unit. Parameter print_RTLBlock: Z -> RTLBlock.program -> unit. Parameter print_RTLPar: Z -> RTLPar.program -> unit. +Parameter print_RTLParFU: Z -> RTLParFU.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. @@ -249,6 +250,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@@ RTLPargen.transl_program @@ print (print_RTLPar 0) @@@ RTLParFUgen.transl_program + @@ print (print_RTLParFU 0) @@@ HTLPargen.transl_program @@ print (print_HTL 0) @@ Veriloggen.transl_program. diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml index ab3c949..0402d49 100644 --- a/src/VericertClflags.ml +++ b/src/VericertClflags.ml @@ -6,6 +6,7 @@ let option_initial = ref false let option_dhtl = ref false let option_drtlblock = ref false let option_drtlpar = ref false +let option_drtlparfu = ref false let option_hls_schedule = ref false let option_fif_conv = ref false let option_fram = ref true diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index bca8fb5..aeefd2a 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -148,6 +148,7 @@ Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if". Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if". Extract Constant Compiler.print_HTL => "PrintHTL.print_if". Extract Constant Compiler.print_RTLPar => "PrintRTLPar.print_if". +Extract Constant Compiler.print_RTLParFU => "PrintRTLParFU.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index b66a704..0695f07 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -392,10 +392,10 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Omulimm n, r::nil => ret (boplit Vmul r n) | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs") | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu") - | Op.Odiv, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: div") - | Op.Odivu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: divu") - | Op.Omod, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mod") - | Op.Omodu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: modu") + | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) + | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) + | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) + | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2) | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2) | Op.Oandimm n, r::nil => ret (boplit Vand r n) | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2) @@ -458,28 +458,6 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := | _ => Error (Errors.msg "Htlgen: add_branch_instr") end. -Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) - (args : list reg) (stack : reg) : mon expr := - match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) - | Mint32, Op.Aindexed off, r1::nil => - if (check_address_parameter_signed off) - then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) - else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") - | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) - if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) - then ret (Vvari stack - (Vbinop Vdivu - (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) - (Vlit (ZToValue 4)))) - else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") - | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) - let a := Integers.Ptrofs.unsigned a in - if (check_address_parameter_unsigned a) - then ret (Vvari stack (Vlit (ZToValue (a / 4)))) - else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset") - | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") - end. - Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := match ns with | n :: ns' => (i, n) :: enumerate (i+1) ns' @@ -680,7 +658,7 @@ Definition translate_predicate (a : assignment) ret (a dst (Vternary (pred_expr preg pos) e dst)) end. -Definition translate_inst a (fin rtrn stack preg : reg) (n : node) (i : instr) +Definition translate_inst a (fin rtrn preg : reg) (n : node) (i : instr) : mon stmnt := match i with | FUnop => @@ -721,18 +699,18 @@ Definition create_new_state (p: node): mon node := s.(st_controllogic)) (create_new_state_state_incr s p). -Definition translate_inst_list (fin rtrn stack preg: reg) (ni : node * node * list (list instr)) := +Definition translate_inst_list (fin rtrn preg: reg) (ni : node * node * list (list instr)) := match ni with | (n, p, li) => do _ <- collectlist (fun l => - do stmnt <- translate_inst Vblock fin rtrn stack preg n l; + do stmnt <- translate_inst Vblock fin rtrn preg n l; add_data_instr n stmnt) (concat li); do st <- get; add_control_instr n (state_goto st.(st_st) p) end. -Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) +Fixpoint translate_cfi' (fin rtrn preg: reg) (cfi: cf_instr) : mon (stmnt * stmnt) := match cfi with | FUgoto n' => @@ -752,8 +730,8 @@ Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) Vskip) end | FUpred_cf p c1 c2 => - do (tc1s, tc1c) <- translate_cfi' fin rtrn stack preg c1; - do (tc2s, tc2c) <- translate_cfi' fin rtrn stack preg c2; + do (tc1s, tc1c) <- translate_cfi' fin rtrn preg c1; + do (tc2s, tc2c) <- translate_cfi' fin rtrn preg c2; ret ((Vcond (pred_expr preg p) tc1s tc2s), (Vcond (pred_expr preg p) tc1c tc2c)) | FUjumptable r tbl => do s <- get; @@ -766,23 +744,23 @@ Fixpoint translate_cfi' (fin rtrn stack preg: reg) (cfi: cf_instr) error (Errors.msg "HTLPargen: RPbuildin not supported.") end. -Definition translate_cfi (fin rtrn stack preg: reg) (ni: node * cf_instr) +Definition translate_cfi (fin rtrn preg: reg) (ni: node * cf_instr) : mon unit := let (n, cfi) := ni in - do (s, c) <- translate_cfi' fin rtrn stack preg cfi; + do (s, c) <- translate_cfi' fin rtrn preg cfi; do _ <- add_control_instr n c; add_data_instr n s. -Definition transf_bblock (fin rtrn stack preg: reg) (ni : node * bblock) +Definition transf_bblock (fin rtrn preg: reg) (ni : node * bblock) : mon unit := let (n, bb) := ni in do nstate <- create_new_state ((poslength bb.(bb_body)))%positive; - do _ <- collectlist (translate_inst_list fin rtrn stack preg) + do _ <- collectlist (translate_inst_list fin rtrn preg) (prange n (nstate + poslength bb.(bb_body) - 1)%positive bb.(bb_body)); match bb.(bb_body) with - | nil => translate_cfi fin rtrn stack preg (n, bb.(bb_exit)) - | _ => translate_cfi fin rtrn stack preg (nstate, bb.(bb_exit)) + | nil => translate_cfi fin rtrn preg (n, bb.(bb_exit)) + | _ => translate_cfi fin rtrn preg (nstate, bb.(bb_exit)) end. Definition decide_order a b c d e f g : {module_ordering a b c d e f g} + {True}. @@ -806,10 +784,8 @@ Definition transf_module (f: function) : mon HTL.module. if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; - do (stack, stack_len) <- create_arr None 32 - (Z.to_nat (f.(fn_stacksize) / 4)); do preg <- create_reg None 32; - do _ <- collectlist (transf_bblock fin rtrn stack preg) + do _ <- collectlist (transf_bblock fin rtrn preg) (Maps.PTree.elements f.(fn_code)); do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(fn_params); diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index 55fe4e7..65ddf74 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -57,7 +57,7 @@ Definition transl_instr (res: resources) (cycle: positive) (i: RTLBlockInstr.ins :: FUop po (Op.Ointconst (Int.repr 0)) nil (ram_wr_en r) :: FUop po (Op.Olea addr) args (ram_addr r) :: FUop po (Op.Oshruimm (Int.repr 2)) ((ram_addr r)::nil) (ram_addr r) - :: instr_list, update (cycle+1) + :: instr_list, update (Pos.pred cycle) (add_instr (FUop po Op.Omove (ram_d_out r::nil) d)) d_tree) | _ => Errors.Error (Errors.msg "Could not find RAM") diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 94225fa..b75465b 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -289,6 +289,7 @@ let comb_delay = function | _ -> 1 let pipeline_stages = function + | RBload _ -> 2 | RBop (_, op, _, _) -> (match op with | Odiv -> 32 @@ -743,7 +744,7 @@ let solve_constraints constr = |> drop 3 |> List.fold_left parse_soln (IMap.empty, IMap.empty) in - Sys.remove fn; res + (*Sys.remove fn;*) res let subgraph dfg l = let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in @@ -806,14 +807,14 @@ let transf_rtlpar c c' schedule = let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) in - (*let body2 = List.fold_left (fun x b -> + let body2 = List.fold_left (fun x b -> match IMap.find_opt b i_sched_tree with | Some i -> i :: x | None -> [] :: x ) [] (range (fst bb_st_e) (snd bb_st_e + 1)) |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) |> List.rev - in*) + in (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) let final_body2 = List.map (fun x -> subgraph dfg x |> (fun x -> @@ -821,7 +822,7 @@ let transf_rtlpar c c' schedule = |> List.map (subgraph x) |> List.map (fun y -> TopoDFG.fold (fun i l -> snd i :: l) y [] - |> List.rev))) body + |> List.rev))) body2 (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x []) |> List.rev) body2*) in |