From 471e2df0abea898607f20ac78c123ff8d9835777 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 10 Aug 2023 11:17:39 +0100 Subject: Add Bambu synthesis and ClockRegisters --- src/hls/ClockRegisters.v | 245 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 245 insertions(+) create mode 100644 src/hls/ClockRegisters.v (limited to 'src') 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 + * + * 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 . + *) + +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. -- cgit