diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:52 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-02-21 21:35:52 +0000 |
commit | a5ae227155f09822207c49d75fdbb6e4b7652936 (patch) | |
tree | 301bdebe77911e0c974d4ffb53b789e5b0e7c931 /src/hls | |
parent | 359194617de51adcc451b45b6c1b0a9332820906 (diff) | |
download | vericert-a5ae227155f09822207c49d75fdbb6e4b7652936.tar.gz vericert-a5ae227155f09822207c49d75fdbb6e4b7652936.zip |
Add operator pipelining pass
Diffstat (limited to 'src/hls')
-rw-r--r-- | src/hls/PipelineOp.v | 67 |
1 files changed, 67 insertions, 0 deletions
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 <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 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. |