diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-10-19 10:02:52 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-10-19 10:02:52 +0100 |
commit | afcb12b5e443da586459455dbc637fc04b9d0634 (patch) | |
tree | 27b55e45ac2f9f790e43dfba4270031064af8ac1 /src/hls/GibleSubPar.v | |
parent | ec4f412f64b93d0bda18cd0f766eb0bf0fb93450 (diff) | |
download | vericert-afcb12b5e443da586459455dbc637fc04b9d0634.tar.gz vericert-afcb12b5e443da586459455dbc637fc04b9d0634.zip |
Add more sub languages
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. |