diff options
Diffstat (limited to 'src/hls/GibleSubPar.v')
-rw-r--r-- | src/hls/GibleSubPar.v | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/src/hls/GibleSubPar.v b/src/hls/GibleSubPar.v new file mode 100644 index 0000000..c867e1b --- /dev/null +++ b/src/hls/GibleSubPar.v @@ -0,0 +1,75 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020-2022 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.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Events. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Smallstep. +Require Import compcert.common.Values. +Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require Import compcert.verilog.Op. +Require Import vericert.hls.Gible. + +(*| +========= +Gible Seq +========= +|*) + +Module SubParBB <: BlockType. + + Definition t := list (list instr). + + Definition foldl (A: Type) (f: A -> instr -> A) (bb : t) (m : A): A := + fold_left + (fun x l => fold_left f l x) + bb m. + + Definition length : t -> nat := @length (list instr). + + Section RELSEM. + + Context {A B: Type} (ge: Genv.t A B). + + Definition step_instr_list := step_list_inter (step_instr ge). + Definition step_instr_seq := step_list step_instr_list. + +(*| +Instruction list step +--------------------- + +The ``step_instr_list`` definition describes the execution of a list of +instructions in one big step, inductively traversing the list of instructions +and applying the ``step_instr``. + +This is simply using the high-level function ``step_list``, which is a general +function that can execute lists of things, given their execution rule. +|*) + + Definition step := step_instr_seq. + + End RELSEM. + +End SubParBB. + +Module GibleSubPar := Gible(SubParBB). +Export GibleSubPar. |