From a5ae227155f09822207c49d75fdbb6e4b7652936 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 21 Feb 2021 21:35:52 +0000 Subject: Add operator pipelining pass --- src/hls/PipelineOp.v | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 src/hls/PipelineOp.v diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v new file mode 100644 index 0000000..0783e4e --- /dev/null +++ b/src/hls/PipelineOp.v @@ -0,0 +1,67 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2021 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 compcert.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.common.Globalenvs. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require Import compcert.verilog.Op. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.RTLPar. +Require Import vericert.hls.FunctionalUnits. + +Definition state : Type := code * funct_units. + +Definition div_pos (il: nat * list nat) x := + let (i, l) := il in + match x with + | RBop _ Odiv _ _ => (S i, i :: l) + | RBop _ Odivu _ _ => (S i, i :: l) + | RBop _ Omod _ _ => (S i, i :: l) + | RBop _ Omodu _ _ => (S i, i :: l) + | _ => (S i, l) + end. + +Definition find_divs (bb: bblock) : list nat := + snd (List.fold_left div_pos bb.(bb_body) (1%nat, nil)). + +Definition transf_code (i: state) (bbn: node * bblock) : state := + let (c, fu) := i in + let (n, bb) := bbn in + (PTree.set n bb c, fu). + +Definition transf_function (f: function) : function := + let (c, fu) := List.fold_left transf_code + (PTree.elements f.(fn_code)) + (PTree.empty bblock, f.(fn_funct_units)) in + mkfunction + f.(fn_sig) + f.(fn_params) + f.(fn_stacksize) + c + fu + f.(fn_entrypoint). + +Definition transf_fundef (fd: fundef) : fundef := + transf_fundef transf_function fd. + +Definition transf_program (p: program) : program := + transform_program transf_fundef p. -- cgit