diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-05-25 18:26:20 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-25 18:26:20 +0100 |
commit | 81618c8d08bd70effcbe3ec087f69106e3cedf95 (patch) | |
tree | 5265bc6bf311c5e744cc52640327cdfb06dad2f2 /src/hls/GiblePar.v | |
parent | b3e2078df318a2d5e54de0b09963f37d63327f0a (diff) | |
download | vericert-81618c8d08bd70effcbe3ec087f69106e3cedf95.tar.gz vericert-81618c8d08bd70effcbe3ec087f69106e3cedf95.zip |
Translate the base languages
Diffstat (limited to 'src/hls/GiblePar.v')
-rw-r--r-- | src/hls/GiblePar.v | 75 |
1 files changed, 75 insertions, 0 deletions
diff --git a/src/hls/GiblePar.v b/src/hls/GiblePar.v new file mode 100644 index 0000000..8eb06ae --- /dev/null +++ b/src/hls/GiblePar.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. + +(*| +======== +RTLBlock +======== +|*) + +Module BB <: BlockType. + + Definition t := list (list (list instr)). + + Section RELSEM. + + Context {A B: Type} (ge: Genv.t A B). + + Definition step_instr_list := step_list (step_instr ge). + Definition step_instr_seq := step_list step_instr_list. + Definition step_instr_block := step_list step_instr_seq. + +(*| +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_block. + + End RELSEM. + + Definition max_reg (m : positive) (pc : node) (bb : t) := + fold_left + (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) + bb m. + + Definition length : t -> nat := @length (list (list instr)). + +End BB. + +Module GiblePar := Gible(BB). |