From d772e22704ffe806b9962507c9faf05ce0159133 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 14 Nov 2021 22:23:06 +0000 Subject: Add proper functional unit generation --- src/hls/RTLParFU.v | 24 +++---------- src/hls/RTLParFUgen.v | 97 ++++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 98 insertions(+), 23 deletions(-) (limited to 'src') diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v index 3442ff0..b18aef6 100644 --- a/src/hls/RTLParFU.v +++ b/src/hls/RTLParFU.v @@ -37,8 +37,8 @@ Definition node := positive. Inductive instr : Type := | FUnop : instr | FUop : option pred_op -> operation -> list reg -> reg -> instr -| FUload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr -| FUstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr +| FUread : positive -> positive -> reg -> instr +| FUwrite : positive -> positive -> reg -> instr | FUsetpred : option pred_op -> condition -> list reg -> predicate -> instr. Inductive cf_instr : Type := @@ -69,10 +69,8 @@ Definition max_reg_instr (m: positive) (i: instr) := | FUnop => m | FUop p op args res => fold_left Pos.max args (Pos.max res m) - | FUload p chunk addr args dst => - fold_left Pos.max args (Pos.max dst m) - | FUstore p chunk addr args src => - fold_left Pos.max args (Pos.max src m) + | FUread p1 p2 r => Pos.max m r + | FUwrite p1 p2 r => Pos.max m r | FUsetpred p' c args p => fold_left Pos.max args m end. @@ -157,7 +155,7 @@ Record function: Type := fn_params: list reg; fn_stacksize: Z; fn_code: code; - fn_funct_units: funct_unit; + fn_funct_units: resources; fn_entrypoint: node; }. @@ -246,18 +244,6 @@ Section RELSEM. eval_operation ge sp op rs##args m = Some v -> eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist -> step_instr sp (mk_instr_state rs pr m) (FUop p op args res) ist - | exec_FUload: - forall addr rs args a chunk m v dst sp p pr ist, - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist -> - step_instr sp (mk_instr_state rs pr m) (FUload p chunk addr args dst) ist - | exec_FUstore: - forall addr rs args a chunk m src m' sp p pr ist, - eval_addressing ge sp addr rs##args = Some a -> - Mem.storev chunk m a rs#src = Some m' -> - eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist -> - step_instr sp (mk_instr_state rs pr m) (FUstore p chunk addr args src) ist | exec_FUsetpred: forall sp rs pr m p c b args p' ist, Op.eval_condition c rs##args m = Some b -> diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index 389d76c..0098f57 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -1,21 +1,110 @@ +(* + * 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 Coq.micromega.Lia. Require Import compcert.common.AST. -Require compcert.common.Errors. +Require Import compcert.common.Errors. Require compcert.common.Globalenvs. -Require compcert.lib.Integers. +Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. Require Import vericert.common.Statemonad. Require Import vericert.common.Vericertlib. Require Import vericert.hls.AssocMap. -Require Import vericert.hls.HTL. Require Import vericert.hls.Predicate. Require Import vericert.hls.RTLParFU. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. Require Import vericert.hls.RTLBlockInstr. Require Import vericert.hls.RTLPar. +Require Import vericert.hls.FunctionalUnits. + +#[local] Open Scope error_monad_scope. + +Definition transl_instr (res: resources) (i: RTLBlockInstr.instr): Errors.res (list (Z * RTLParFU.instr)) := + match i with + | RBnop => Errors.OK ((0, FUnop)::nil) + | RBop po op args d => Errors.OK ((0, FUop po op args d)::nil) + | RBload po chunk addr args d => + match get_ram 0 res with + | Some (ri, r) => + Errors.OK ((0, FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r)) + :: (0, FUop po (Op.Ointconst (Int.repr 0)) nil (ram_wr_en r)) + :: (0, FUop po (Op.Olea addr) args (ram_addr r)) + :: (1, FUop po Op.Omove (ram_d_out r::nil) d) + :: nil) + | _ => Errors.Error (Errors.msg "Could not find RAM") + end + | RBstore po chunk addr args d => + match get_ram 0 res with + | Some (ri, r) => + Errors.OK ((0, FUop po Op.Onot (ram_u_en r::nil) (ram_u_en r)) + :: (0, FUop po (Op.Ointconst (Int.repr 1)) nil (ram_wr_en r)) + :: (0, FUop po Op.Omove (d::nil) (ram_d_in r)) + :: (0, FUop po (Op.Olea addr) args (ram_addr r)) + :: nil) + | _ => Errors.Error (Errors.msg "Could not find RAM") + end + | RBsetpred op c args p => Errors.OK ((0, FUsetpred op c args p)::nil) + end. + +Fixpoint transl_cf_instr (i: RTLBlockInstr.cf_instr): RTLParFU.cf_instr := + match i with + | RBcall sig r args d n => FUcall sig r args d n + | RBtailcall sig r args => FUtailcall sig r args + | RBbuiltin ef args r n => FUbuiltin ef args r n + | RBcond c args n1 n2 => FUcond c args n1 n2 + | RBjumptable r ns => FUjumptable r ns + | RBreturn r => FUreturn r + | RBgoto n => FUgoto n + | RBpred_cf po c1 c2 => FUpred_cf po (transl_cf_instr c1) (transl_cf_instr c2) + end. + +Definition list_split {A:Type} (l: list (Z * A)) : (list (Z * A)) * (list (Z * A)) := + (filter (fun x => Z.eqb 0 (fst x)) l, + map (fun x => (Z.pred (fst x), snd x)) (filter (fun x => negb (Z.eqb 0 (fst x))) l)). + +Fixpoint map_error {A B : Type} (f : A -> res B) (l : list A) {struct l} : res (list B) := + match l with + | nil => OK nil + | x::xs => + do y <- f x ; + do ys <- map_error f xs ; + OK (y::ys) + end. + +Definition transl_bb (res: resources) (bb: RTLPar.bb): RTLParFU.bblock_body := + map_error (map_error (fold_right + (fun c n => transl_instr res))) bb. + +Definition transl_bblock (bb: RTLPar.bblock): RTLParFU.bblock := + RTLParFU.mk_bblock (transl_bb (bb_body bb)) (transl_cf_instr (bb_exit bb)). + +Definition transl_code (c: RTLPar.code): RTLParFU.code := + PTree.map (fun _ => transl_bblock) c. + +Definition transl_function (f: RTLPar.function): Errors.res RTLParFU.function := + Errors.OK (RTLParFU.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (transl_code (fn_code f)) + initial_resources (fn_entrypoint f)). + +Definition transl_fundef p := + transf_partial_fundef transl_function p. -Definition transl_program (p : RTLParFU.program) : Errors.res HTL.program := +Definition transl_program (p : RTLPar.program) : Errors.res RTLParFU.program := transform_partial_program transl_fundef p. -- cgit