diff options
m--------- | docs | 0 | ||||
-rw-r--r-- | src/hls/HTLgenproof.v | 22 | ||||
-rw-r--r-- | src/hls/RTLPargenproof.v | 60 |
3 files changed, 78 insertions, 4 deletions
diff --git a/docs b/docs -Subproject 1ff8b1c7a3f3e37809e9ac8c1e21d50df270696 +Subproject a596c0c469d7c61b5ed8dfaf8805a926024a3a7 diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index f2de2d9..9a7e272 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -17,10 +17,24 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From compcert Require RTL Registers AST. -From compcert Require Import Integers Globalenvs Memory Linking. -From vericert Require Import Vericertlib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. -From vericert Require HTL Verilog. +Require compcert.backend.RTL. +Require compcert.backend.Registers. +Require compcert.common.AST. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Linking. +Require Import compcert.common.Memory. +Require Import compcert.lib.Integers. + +Require Import vericert.common.IntegerExtra. +Require Import vericert.common.Vericertlib. +Require Import vericert.common.ZExtra. +Require Import vericert.hls.Array. +Require Import vericert.hls.AssocMap. +Require vericert.hls.HTL. +Require Import vericert.hls.HTLgen. +Require Import vericert.hls.HTLgenspec. +Require Import vericert.hls.ValueInt. +Require vericert.hls.Verilog. Require Import Lia. diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v new file mode 100644 index 0000000..05001ce --- /dev/null +++ b/src/hls/RTLPargenproof.v @@ -0,0 +1,60 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2021 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.common.AST. +Require Import compcert.common.Errors. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.RTLPar. +Require Import vericert.hls.RTLPargen. +Require Import vericert.hls.Scheduleoracle. + +Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := +| match_stackframe: + forall f tf res sp pc rs, + transl_function f = OK tf -> + match_stackframes (RTLBlock.Stackframe res f sp pc rs) + (RTLPar.Stackframe res tf sp pc rs). + +Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := +| match_state: + forall sf f sp pc rs mem sf' tf + (TRANSL: transl_function f = OK tf) + (STACKS: list_forall2 match_stackframes sf sf'), + match_states (RTLBlock.State sf f sp pc rs mem) + (RTLPar.State sf' tf sp pc rs mem) +| match_block: + forall sf sf' f tf sp cfi rs mem + (TRANSL: transl_function f = OK tf) + (STACKS: list_forall2 match_stackframes sf sf'), + match_states (RTLBlock.Block sf f sp cfi rs mem) + (RTLPar.Block sf' tf sp (mk_bblock nil cfi) rs mem) +| match_returnstate: + forall stack stack' v mem + (STACKS: list_forall2 match_stackframes stack stack'), + match_states (RTLBlock.Returnstate stack v mem) + (RTLPar.Returnstate stack' v mem) +| match_initial_call: + forall stack stack' f tf args m + (TRANSL: transl_fundef f = OK tf) + (STACKS: list_forall2 match_stackframes stack stack'), + match_states (RTLBlock.Callstate stack f args m) + (RTLPar.Callstate stack' tf args m). |