diff options
-rw-r--r-- | benchmarks/polybench-syn/common.mk | 7 | ||||
-rw-r--r-- | driver/VericertDriver.ml | 2 | ||||
-rwxr-xr-x | scripts/synth-ssh.sh | 12 | ||||
-rwxr-xr-x | scripts/synth.sh | 6 | ||||
-rw-r--r-- | scripts/synth.tcl | 2 | ||||
-rwxr-xr-x | scripts/synthesis-results.scm | 2 | ||||
-rw-r--r-- | src/Compiler.v | 27 | ||||
-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 |
13 files changed, 114 insertions, 66 deletions
diff --git a/benchmarks/polybench-syn/common.mk b/benchmarks/polybench-syn/common.mk index 877dd68..a0b01d4 100644 --- a/benchmarks/polybench-syn/common.mk +++ b/benchmarks/polybench-syn/common.mk @@ -32,10 +32,17 @@ all: $(TARGETS) clean: rm -f *.iver rm -f *.v + rm -f *.sv rm -f *.gcc rm -f *.clog rm -f *.tmp rm -f $(TARGETS) + rm -f *.{0,1,2,3,4,5,6,7,8,9} + rm -f *.smt2 + rm -f *.log + rm -f *.dot + rm -f *.vtlog + rm -f *.txt rm -rf *.verilator .PRECIOUS: %.v %.gcc %.iver diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 87ce2c6..5950e95 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -98,7 +98,7 @@ let compile_c_file sourcename ifile ofile = then Vericert.Compiler0.transf_hls_temp else Vericert.Compiler0.transf_hls in - let _ = Vericert.Smtpredicate.check_smt (Vericert.Predicate0.Pimp ((Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)),(Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)))) in + (* let _ = Vericert.Smtpredicate.check_smt (Vericert.Predicate0.Pimp ((Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)),(Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)))) in *) match translation csyntax with | Vericert.Errors.OK v -> if !Vericert.Cohpred.cohpred_counter > 0 then Printf.fprintf stderr "OK\n"; v diff --git a/scripts/synth-ssh.sh b/scripts/synth-ssh.sh index a6ce349..ca255e1 100755 --- a/scripts/synth-ssh.sh +++ b/scripts/synth-ssh.sh @@ -1,4 +1,4 @@ -#!/usr/bin/bash +#!/usr/bin/env bash # Assumes that the Verilog is passed on the command line, that the tcl file is in synth.tcl and # returns encode_report.xml. @@ -10,19 +10,19 @@ bench=$2 output=$3 machine=ee-beholder${num}.ee.ic.ac.uk user=ymh15 -files="$scriptsdir/synth.tcl $output/$bench.v" +files="$scriptsdir/synth.tcl $output/$bench.sv" log="$output/${bench}_synth.log" date >$log -temp=$(ssh $user@$machine "mktemp -d" 2>>$log) +temp=$(ssh $user@$machine "mktemp -d") >&2 echo "synthesising $bench $temp" rsync $files $user@$machine:$temp/ >>$log 2>&1 ssh $user@$machine \ - "bash -lc 'cd $temp && cp $(basename $bench).v main.v && vivado -mode batch -source synth.tcl'" \ + "bash -lc 'cd $temp && cp $(basename $bench).sv main.sv && vivado -mode batch -source synth.tcl'" \ >>$log 2>&1 rsync $user@$machine:$temp/encode_report.xml $output/${bench}_report.xml >>$log 2>&1 -ssh $user@$machine "rm -rf '$temp'" >>$log 2>&1 -rm -f main.v >>$log 2>&1 +# ssh $user@$machine "rm -rf '$temp'" >>$log 2>&1 +rm -f main.sv >>$log 2>&1 >&2 echo "done $bench" diff --git a/scripts/synth.sh b/scripts/synth.sh index b1c2696..d459dd3 100755 --- a/scripts/synth.sh +++ b/scripts/synth.sh @@ -1,4 +1,4 @@ -#!/usr/bin/bash +#!/usr/bin/env bash set -x @@ -24,9 +24,9 @@ fi echo "copying directory structure from $source to $output" mkdir -p $output -rsync -am --include '*/' --include '*.v' --exclude '*' $source/ $output/ +rsync -am --include '*/' --include '*.sv' --exclude '*' $source/ $output/ echo "executing $parallel runs in parallel" -cat $scriptsdir/../benchmarks/polybench-syn/benchmark-list-master | \ +cat ./benchmark-list-master | \ xargs --max-procs=$parallel --replace=% \ $scriptsdir/synth-ssh.sh 0 % $output diff --git a/scripts/synth.tcl b/scripts/synth.tcl index a2fb722..f5a2388 100644 --- a/scripts/synth.tcl +++ b/scripts/synth.tcl @@ -76,7 +76,7 @@ proc dump_statistics { } { }; #END PROC set outputDir . create_project -in_memory -part xc7z020clg484-1 -force -read_verilog -sv main.v +read_verilog -sv main.sv synth_design -mode out_of_context -no_iobuf -top main -part xc7z020clg484-1 write_checkpoint -force $outputDir/post_synth.dcp report_timing_summary -file $outputDir/post_synth_timing_summary.rpt diff --git a/scripts/synthesis-results.scm b/scripts/synthesis-results.scm index b1a7349..3760cfb 100755 --- a/scripts/synthesis-results.scm +++ b/scripts/synthesis-results.scm @@ -1,4 +1,4 @@ -#! /usr/bin/chicken-csi -ss +#! /usr/local/bin/csi -ss ;; -*- mode: scheme -*- ;; ;; Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> diff --git a/src/Compiler.v b/src/Compiler.v index a674866..d76db43 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -74,6 +74,7 @@ Require vericert.hls.DeadBlocks. Require vericert.HLSOpts. Require vericert.hls.Memorygen. Require vericert.hls.DMemorygen. +Require vericert.hls.ClockRegisters. Require Import vericert.hls.HTLgenproof. @@ -230,8 +231,8 @@ Definition transf_backend (r : RTL.program) : res Verilog.program := @@ print (print_RTL 7) @@@ HTLgen.transl_program @@ print (print_HTL 0) -(* @@ total_if HLSOpts.optim_ram Memorygen.transf_program - @@ print (print_HTL 1)*) + @@ total_if HLSOpts.optim_ram Memorygen.transf_program + @@ print (print_HTL 1) @@ Veriloggen.transl_program. (*| @@ -297,7 +298,9 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@@ HTLPargen.transl_program @@ print (print_DHTL 0) @@ DMemorygen.transf_program - @@ print (print_DHTL 0) + @@ print (print_DHTL 1) + @@@ ClockRegisters.transl_program + @@ print (print_DHTL 2) @@ DVeriloggen.transl_program. (*| @@ -326,7 +329,7 @@ Definition CompCert's_passes := ::: mkpass Unusedglobproof.match_prog ::: (@mkpass _ _ HTLgenproof.match_prog (HTLgenproof.TransfHTLLink HTLgen.transl_program)) - (*::: mkpass (match_if HLSOpts.optim_ram Memorygen.match_prog)*) + ::: mkpass (match_if HLSOpts.optim_ram Memorygen.match_prog) ::: mkpass Veriloggenproof.match_prog ::: pass_nil _. @@ -380,8 +383,8 @@ Proof. simpl in T; try discriminate. destruct (HTLgen.transl_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate. - (*set (p15 := total_if HLSOpts.optim_ram Memorygen.transf_program p14) in *.*) - set (p15 := Veriloggen.transl_program p14) in *. + set (p15 := total_if HLSOpts.optim_ram Memorygen.transf_program p14) in *. + set (p16 := Veriloggen.transl_program p15) in *. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -401,9 +404,9 @@ Proof. apply Deadcodeproof.transf_program_match. exists p13; split. apply Unusedglobproof.transf_program_match; auto. exists p14; split. apply HTLgenproof.transf_program_match; auto. - (*exists p15; split. apply total_if_match. - apply Memorygen.transf_program_match; auto.*) - exists p15; split. apply Veriloggenproof.transf_program_match; auto. + exists p15; split. apply total_if_match. + apply Memorygen.transf_program_match; auto. + exists p16; split. apply Veriloggenproof.transf_program_match; auto. inv T. reflexivity. Qed. @@ -423,7 +426,7 @@ Ltac DestructM := end. repeat DestructM. subst tp. assert (F: forward_simulation (Cstrategy.semantics p) - (Verilog.semantics p15)). + (Verilog.semantics p16)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -457,9 +460,9 @@ Ltac DestructM := eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply HTLgenproof.transf_program_correct. eassumption. - (*eapply compose_forward_simulations. + eapply compose_forward_simulations. eapply match_if_simulation. eassumption. - exact Memorygen.transf_program_correct; eassumption.*) + exact Memorygen.transf_program_correct; eassumption. eapply Veriloggenproof.transf_program_correct; eassumption. } split. auto. 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. *) |