diff options
Diffstat (limited to 'src/hls/GibleSubPargen.v')
-rw-r--r-- | src/hls/GibleSubPargen.v | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/src/hls/GibleSubPargen.v b/src/hls/GibleSubPargen.v new file mode 100644 index 0000000..a6dfa4a --- /dev/null +++ b/src/hls/GibleSubPargen.v @@ -0,0 +1,63 @@ +(* + * 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.micromega.Lia. + +Require Import compcert.lib.Maps. +Require Import compcert.common.Errors. +Require compcert.common.Globalenvs. +Require compcert.lib.Integers. +Require Import compcert.common.AST. + +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.Verilog. +Require Import vericert.hls.Gible. +Require Import vericert.hls.GibleSubPar. +Require Import vericert.hls.GiblePar. +Require Import vericert.hls.Predicate. +Require Import vericert.common.Errormonad. +Import ErrorMonad. +Import ErrorMonadExtra. +Import MonadNotation. + +#[local] Open Scope monad_scope. + +Definition transl_block' (icode: positive * (positive * GibleSubPar.code)) (bb: SubParBB.t): + res (positive * (positive * GibleSubPar.code)) := + let '(curr, (next, code)) := icode in + match code ! curr with + | None => OK (next, (Pos.succ next, PTree.set curr (bb ++ (((RBexit None (RBgoto next))::nil)::nil)) code)) + | _ => Error (msg "GibleSubPargen: Overlapping blocks in translation") + end. + +Definition transl_block (freshcode: positive * GibleSubPar.code) (ibb: positive * ParBB.t): res (positive * GibleSubPar.code) := + let (i, bb) := ibb in + let (fresh, code) := freshcode in + map snd (mfold_left transl_block' bb (OK (i, (fresh, code)))). + +Definition transl_function (f: GiblePar.function) : res GibleSubPar.function := + do new_code <- mfold_left transl_block (PTree.elements f.(fn_code)) (OK (Pos.succ (max_pc_function f), PTree.empty _)); + OK (GibleSubPar.mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) (snd new_code) f.(fn_entrypoint)). + +Definition transl_fundef := transf_partial_fundef transl_function. + +Definition transl_program (p : GiblePar.program) : Errors.res GibleSubPar.program := + transform_partial_program transl_fundef p. |