Fix backend hardware generation and scheduling

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. *)