Add Bambu synthesis and ClockRegisters

4 files changed, 414 insertions, 0 deletions

diff --git a/scripts/synth-bambu.sh b/scripts/synth-bambu.sh
new file mode 100755
index 0000000..490190e
--- /dev/null
+++ b/scripts/synth-bambu.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+set -x
+
+scriptsdir=$(dirname "$(readlink -f "$BASH_SOURCE")")
+
+if [[ -z "$1" ]]; then
+    parallel=1
+else
+    parallel=$1
+fi
+
+if [[ -z "$2" ]]; then
+    output=$(pwd)
+else
+    output=$2
+fi
+
+if [[ -z "$3" ]]; then
+    source=$(pwd)
+else
+    source=$3
+fi
+
+echo "copying directory structure from $source to $output"
+mkdir -p $output
+rsync -am --include '*/' --include '*.v' --exclude '*' $source/ $output/
+
+echo "executing $parallel runs in parallel"
+cat ./benchmark-list-master | \
+    xargs --max-procs=$parallel --replace=% \
+    $scriptsdir/synth-ssh-bambu.sh 0 % $output
diff --git a/scripts/synth-bambu.tcl b/scripts/synth-bambu.tcl
new file mode 100644
index 0000000..82ce12e
--- /dev/null
+++ b/scripts/synth-bambu.tcl
@@ -0,0 +1,109 @@
+proc dump_statistics {  } {
+  set util_rpt [report_utilization -return_string]
+  set LUTFFPairs 0
+  set SliceRegisters 0
+  set Slice 0
+  set SliceLUTs 0
+  set SliceLUTs1 0
+  set BRAMFIFO36 0
+  set BRAMFIFO18 0
+  set BRAMFIFO36_star 0
+  set BRAMFIFO18_star 0
+  set BRAM18 0
+  set BRAMFIFO 0
+  set BIOB 0
+  set DSPs 0
+  set TotPower 0
+  set design_slack 0
+  set design_req 0
+  set design_delay 0
+  regexp --  {\s*LUT Flip Flop Pairs\s*\|\s*([^[:blank:]]+)} $util_rpt ignore LUTFFPairs
+  regexp --  {\s*Slice Registers\s*\|\s*([^[:blank:]]+)} $util_rpt ignore SliceRegisters
+  regexp --  {\s*Slice\s*\|\s*([^[:blank:]]+)} $util_rpt ignore Slice
+  regexp --  {\s*Slice LUTs\s*\|\s*([^[:blank:]]+)} $util_rpt ignore SliceLUTs
+  regexp --  {\s*Slice LUTs\*\s*\|\s*([^[:blank:]]+)} $util_rpt ignore SliceLUTs1
+  if { [expr {$LUTFFPairs == 0}] } {
+    set LUTFFPairs $SliceLUTs1
+    puts $SliceLUTs1
+  }
+  if { [expr {$SliceLUTs == 0}] } {
+    set SliceLUTs $SliceLUTs1
+  }
+  regexp --  {\s*RAMB36/FIFO36\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAMFIFO36
+  regexp --  {\s*RAMB18/FIFO18\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAMFIFO18
+  regexp --  {\s*RAMB36/FIFO\*\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAMFIFO36_star
+  regexp --  {\s*RAMB18/FIFO\*\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAMFIFO18_star
+  regexp --  {\s*RAMB18\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BRAM18
+  set BRAMFIFO [expr {(2 *$BRAMFIFO36) + $BRAMFIFO18 + (2*$BRAMFIFO36_star) + $BRAMFIFO18_star + $BRAM18}]
+  regexp --  {\s*Bonded IOB\s*\|\s*([^[:blank:]]+)} $util_rpt ignore BIOB
+  regexp --  {\s*DSPs\s*\|\s*([^[:blank:]]+)} $util_rpt ignore DSPs
+  set power_rpt [report_power -return_string]
+  regexp --  {\s*Total On-Chip Power \(W\)\s*\|\s*([^[:blank:]]+)} $power_rpt ignore TotPower
+  set Timing_Paths [get_timing_paths -max_paths 1 -nworst 1 -setup]
+  if { [expr {$Timing_Paths == ""}] } {
+    set design_slack 0
+    set design_req 0
+  } else {
+    set design_slack [get_property SLACK $Timing_Paths]
+    set design_req [get_property REQUIREMENT  $Timing_Paths]
+  }
+  if { [expr {$design_slack == ""}] } {
+    set design_slack 0
+  }
+  if { [expr {$design_req == ""}] } {
+    set design_req 0
+  }
+  set design_delay [expr {$design_req - $design_slack}]
+  file delete -force encode_report.xml
+  set ofile_report [open encode_report.xml w]
+  puts $ofile_report "<?xml version=\"1.0\"?>"
+  puts $ofile_report "<document>"
+  puts $ofile_report "  <application>"
+  puts $ofile_report "    <section stringID=\"XILINX_SYNTHESIS_SUMMARY\">"
+  puts $ofile_report "      <item stringID=\"XILINX_LUT_FLIP_FLOP_PAIRS_USED\" value=\"$LUTFFPairs\"/>"
+  puts $ofile_report "      <item stringID=\"XILINX_SLICE\" value=\"$Slice\"/>"
+  puts $ofile_report "      <item stringID=\"XILINX_SLICE_REGISTERS\" value=\"$SliceRegisters\"/>"
+  puts $ofile_report "      <item stringID=\"XILINX_SLICE_LUTS\" value=\"$SliceLUTs\"/>"
+  puts $ofile_report "      <item stringID=\"XILINX_BLOCK_RAMFIFO\" value=\"$BRAMFIFO\"/>"
+  puts $ofile_report "      <item stringID=\"XILINX_IOPIN\" value=\"$BIOB\"/>"
+  puts $ofile_report "      <item stringID=\"XILINX_DSPS\" value=\"$DSPs\"/>"
+  puts $ofile_report "      <item stringID=\"XILINX_POWER\" value=\"$TotPower\"/>"
+  puts $ofile_report "      <item stringID=\"XILINX_DESIGN_DELAY\" value=\"$design_delay\"/>"
+  puts $ofile_report "    </section>"
+  puts $ofile_report "  </application>"
+  puts $ofile_report "</document>"
+  close $ofile_report
+}; #END PROC
+set outputDir .
+create_project -in_memory -part xc7z020clg484-1 -force
+read_verilog -sv main_top.v
+synth_design -mode out_of_context -no_iobuf -top main_top -part xc7z020clg484-1
+write_checkpoint -force $outputDir/post_synth.dcp
+report_timing_summary -file $outputDir/post_synth_timing_summary.rpt
+report_utilization -file $outputDir/post_synth_util.rpt
+create_clock -name clock -period 10.000 [get_ports clock]
+dump_statistics
+opt_design
+dump_statistics
+report_utilization -file $outputDir/post_opt_design_util.rpt
+place_design -directive Explore
+report_clock_utilization -file $outputDir/clock_util.rpt
+# Optionally run optimization if there are timing violations after placement
+if {[get_property SLACK [get_timing_paths -max_paths 1 -nworst 1 -setup]] < 0.5} {
+  puts "Found setup timing violations => running physical optimization"
+  phys_opt_design
+}
+write_checkpoint -force $outputDir/post_place.dcp
+report_utilization -file $outputDir/post_place_util.rpt
+report_timing_summary -file $outputDir/post_place_timing_summary.rpt
+dump_statistics
+route_design -directive Explore
+write_checkpoint -force $outputDir/post_route.dcp
+report_route_status -file $outputDir/post_route_status.rpt
+report_timing_summary -file $outputDir/post_route_timing_summary.rpt
+report_power -file $outputDir/post_route_power.rpt
+report_drc -file $outputDir/post_imp_drc.rpt
+report_utilization -file $outputDir/post_route_util.rpt
+dump_statistics
+close_design
+close_project
diff --git a/scripts/synth-ssh-bambu.sh b/scripts/synth-ssh-bambu.sh
new file mode 100755
index 0000000..5bc1a4d
--- /dev/null
+++ b/scripts/synth-ssh-bambu.sh
@@ -0,0 +1,28 @@
+#!/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.
+
+scriptsdir=$(dirname "$(readlink -f "$BASH_SOURCE")")
+
+num=$1
+bench=$2
+output=$3
+machine=ee-beholder${num}.ee.ic.ac.uk
+user=ymh15
+files="$scriptsdir/synth-bambu.tcl $output/$bench/main_top.v"
+log="$output/${bench}_synth.log"
+
+date >$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 && vivado -mode batch -source synth-bambu.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.sv >>$log 2>&1
+>&2 echo "done $bench"
diff --git a/src/hls/ClockRegisters.v b/src/hls/ClockRegisters.v
new file mode 100644
index 0000000..4b1c37a
--- /dev/null
+++ b/src/hls/ClockRegisters.v
@@ -0,0 +1,245 @@
+(*
+ * Vericert: Verified high-level synthesis.
+ * 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
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+Require Import Coq.FSets.FMapPositive.
+Require Import Coq.micromega.Lia.
+
+Require compcert.common.Events.
+Require compcert.common.Globalenvs.
+Require compcert.common.Smallstep.
+Require compcert.common.Values.
+Require Import compcert.lib.Integers.
+Require Import compcert.lib.Maps.
+Require Import compcert.common.AST.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.Array.
+Require Import vericert.hls.DHTL.
+Require Import vericert.common.Monad.
+Require Import vericert.common.Optionmonad.
+Require vericert.hls.Verilog.
+
+Import OptionExtra.
+
+#[local] Open Scope monad_scope.
+
+Definition pred := positive.
+
+Inductive lhs : Type :=
+| LhsReg : reg -> lhs
+| LhsPred : pred -> lhs
+.
+
+Definition lhs_eqd (r1 r2: lhs): {r1 = r2} + {r1 <> r2}.
+  pose proof peq.
+  decide equality.
+Defined.
+
+Module R_indexed.
+  Definition t := lhs.
+  Definition index (rs: t) : positive :=
+    match rs with
+    | LhsReg r => xO r
+    | LhsPred p => xI p
+    end.
+
+  Lemma index_inj:  forall (x y: t), index x = index y -> x = y.
+  Proof. destruct x; destruct y; crush. Qed.
+
+  Definition eq := lhs_eqd.
+End R_indexed.
+
+Module RTree := ITree(R_indexed).
+
+Inductive flat_expr : Type :=
+| FVlit : value -> flat_expr
+| FVvar : lhs -> flat_expr
+| FVbinop : Verilog.binop -> flat_expr -> flat_expr -> flat_expr
+| FVunop : Verilog.unop -> flat_expr -> flat_expr
+| FVternary : flat_expr -> flat_expr -> flat_expr -> flat_expr
+.
+
+Inductive flat_stmnt : Type :=
+| FVblock : lhs -> flat_expr -> flat_stmnt
+| FVnonblock : lhs -> flat_expr -> flat_stmnt
+.
+
+Fixpoint flatten_expr (preg: reg) (e: Verilog.expr) : option flat_expr :=
+  match e with
+  | Verilog.Vlit v => Some (FVlit v)
+  | Verilog.Vvar r => Some (FVvar (LhsReg r))
+  | Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2) =>
+    if Pos.eqb preg r && Int.eq i1 i2 then
+      match Int.unsigned i1 with
+      | Zpos p => Some (FVvar (LhsPred p))
+      | _ => None
+      end
+    else None
+  | Verilog.Vunop u e => 
+    match flatten_expr preg e with
+    | Some fe => Some (FVunop u fe)
+    | _ => None
+    end
+  | Verilog.Vbinop u e1 e2 => 
+    match flatten_expr preg e1, flatten_expr preg e2 with
+    | Some fe1, Some fe2 => Some (FVbinop u fe1 fe2)
+    | _, _ => None
+    end
+  | Verilog.Vternary e1 e2 e3 => 
+    match flatten_expr preg e1, flatten_expr preg e2, flatten_expr preg e3 with
+    | Some fe1, Some fe2, Some fe3 => Some (FVternary fe1 fe2 fe3)
+    | _, _, _ => None
+    end
+  | _ => None
+  end.
+
+Fixpoint flatten_seq_block (preg: reg) (s: Verilog.stmnt) : option (list flat_stmnt) := 
+  match s with
+  | Verilog.Vskip => Some nil
+  | Verilog.Vseq s1 s2 =>
+    match flatten_seq_block preg s1, flatten_seq_block preg s2 with
+    | Some s1', Some s2' => 
+      Some (s1' ++ s2')
+    | _, _ => None
+    end
+  | Verilog.Vblock (Verilog.Vvar r) e => 
+    match flatten_expr preg e with 
+    | Some fe => Some (FVblock (LhsReg r) fe :: nil)
+    | _ => None
+    end
+  | Verilog.Vblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e => 
+    if Pos.eqb preg r && Int.eq i1 i2 then
+      match Int.unsigned i1, flatten_expr preg e with 
+      | Zpos p, Some fe => Some (FVblock (LhsPred p) fe :: nil)
+      | _, _ => None
+      end
+    else None
+  | Verilog.Vnonblock (Verilog.Vvar r) e => 
+    match flatten_expr preg e with 
+    | Some fe => Some (FVnonblock (LhsReg r) fe :: nil)
+    | _ => None
+    end
+  | Verilog.Vnonblock (Verilog.Vrange r (Verilog.Vlit i1) (Verilog.Vlit i2)) e => 
+    if Pos.eqb preg r && Int.eq i1 i2 then
+      match Int.unsigned i1, flatten_expr preg e with 
+      | Zpos p, Some fe => Some (FVnonblock (LhsPred p) fe :: nil)
+      | _, _ => None
+      end
+    else None
+  | _ => None
+  end.
+
+Fixpoint expand_expr (preg: reg) (f: flat_expr): Verilog.expr :=
+  match f with
+  | FVlit l => Verilog.Vlit l
+  | FVvar (LhsReg r) => Verilog.Vvar r
+  | FVvar (LhsPred p) => Verilog.Vrange preg (Verilog.Vlit (Int.repr (Zpos p))) (Verilog.Vlit (Int.repr (Zpos p)))
+  | FVbinop b e1 e2 => Verilog.Vbinop b (expand_expr preg e1) (expand_expr preg e2)
+  | FVunop b e => Verilog.Vunop b (expand_expr preg e)
+  | FVternary e1 e2 e3 => Verilog.Vternary (expand_expr preg e1) (expand_expr preg e2) (expand_expr preg e3)
+  end.
+
+Definition expand_assignment (preg: reg) (f: flat_stmnt): Verilog.stmnt := 
+  match f with
+  | FVblock (LhsReg r) e => Verilog.Vblock (Verilog.Vvar r) (expand_expr preg e)
+  | FVnonblock (LhsReg r) e => Verilog.Vnonblock (Verilog.Vvar r) (expand_expr preg e)
+  | FVblock (LhsPred p) e => 
+    Verilog.Vblock (Verilog.Vrange preg (Verilog.Vlit (Int.repr (Zpos p))) 
+      (Verilog.Vlit (Int.repr (Zpos p)))) (expand_expr preg e)
+  | FVnonblock (LhsPred p) e => 
+    Verilog.Vnonblock (Verilog.Vrange preg (Verilog.Vlit (Int.repr (Zpos p))) 
+      (Verilog.Vlit (Int.repr (Zpos p)))) (expand_expr preg e)
+  end.
+
+Definition fold_seq_block (preg: reg) (s: list flat_stmnt): Verilog.stmnt :=
+  fold_left (fun a b => Verilog.Vseq a (expand_assignment preg b)) s Verilog.Vskip.
+
+Fixpoint clock_expr (t: RTree.t flat_expr) (f: flat_expr): flat_expr :=
+  match f with
+  | FVvar r => 
+    match RTree.get r t with
+    | Some e => e
+    | None => FVvar r
+    end
+  | FVunop b e => FVunop b (clock_expr t e)
+  | FVbinop b e1 e2 => 
+    FVbinop b (clock_expr t e1) (clock_expr t e2)
+  | FVternary e1 e2 e3 => 
+    FVternary (clock_expr t e1) (clock_expr t e2) (clock_expr t e3)
+  | _ => f
+  end.
+
+Definition clock_assignment (tl: RTree.t flat_expr * list flat_stmnt) (f: flat_stmnt): 
+    (RTree.t flat_expr * list flat_stmnt) :=
+  let (t, l) := tl in
+  match f with
+  | FVblock r e => 
+    let fe := clock_expr t e in 
+    (RTree.set r fe t, l ++ (FVnonblock r fe :: nil))
+  | _ => (t, l ++ (f :: nil))
+  end.
+
+Definition clock_assignments (s: list flat_stmnt): list flat_stmnt :=
+  snd (fold_left clock_assignment s (RTree.empty _, nil)).
+
+Definition clock_stmnt_assignments (preg: reg) (s: Verilog.stmnt): option Verilog.stmnt :=
+  match flatten_seq_block preg s with
+  | Some fs => Some (fold_seq_block preg (clock_assignments fs))
+  | None => None
+  end.
+
+Program Definition transf_module (m: DHTL.module) : option DHTL.module :=
+  match (PTree.fold (fun b i a => 
+           match b, clock_stmnt_assignments m.(mod_preg) a with 
+           | Some tb, Some a' => Some (PTree.set i a' tb)
+           | _, _ => None
+           end)) m.(mod_datapath) (Some (PTree.empty _)) with
+  | Some dp =>
+    Some (mkmodule m.(mod_params)
+      dp
+      m.(mod_entrypoint)
+      m.(mod_st)
+      m.(mod_stk)
+      m.(mod_stk_len)
+      m.(mod_finish)
+      m.(mod_return)
+      m.(mod_start)
+      m.(mod_reset)
+      m.(mod_clk)
+      m.(mod_preg)
+      m.(mod_scldecls)
+      m.(mod_arrdecls)
+      m.(mod_ram) 
+      _
+      m.(mod_ordering_wf)
+      m.(mod_ram_wf)
+      m.(mod_params_wf))
+  | _ => None
+  end.
+Next Obligation.
+Admitted.
+
+Definition transl_module (m : DHTL.module) : Errors.res DHTL.module :=
+  Verilog.handle_opt (Errors.msg "ClockRegisters: not translated") (transf_module m).
+
+Definition transl_fundef := transf_partial_fundef transl_module.
+
+Definition transl_program (p : DHTL.program) : Errors.res DHTL.program :=
+  transform_partial_program transl_fundef p.