diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:39 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:39 +0100 |
commit | 471e2df0abea898607f20ac78c123ff8d9835777 (patch) | |
tree | 50819c77c3a74761208d9ff7a2dc9507585cfef9 | |
parent | b32e7574864cde80f8f5283431c21a6803a89108 (diff) | |
download | vericert-471e2df0abea898607f20ac78c123ff8d9835777.tar.gz vericert-471e2df0abea898607f20ac78c123ff8d9835777.zip |
Add Bambu synthesis and ClockRegisters
-rwxr-xr-x | scripts/synth-bambu.sh | 32 | ||||
-rw-r--r-- | scripts/synth-bambu.tcl | 109 | ||||
-rwxr-xr-x | scripts/synth-ssh-bambu.sh | 28 | ||||
-rw-r--r-- | src/hls/ClockRegisters.v | 245 |
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. |