From 32f0f542c18b73303613b53573e6c61bc7ae6890 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 May 2020 23:14:48 +0100 Subject: Add match_states Inductive --- src/translation/HTLgenproof.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 src/translation/HTLgenproof.v (limited to 'src') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v new file mode 100644 index 0000000..898fafd --- /dev/null +++ b/src/translation/HTLgenproof.v @@ -0,0 +1,29 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * 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 . + *) + +From coqup Require Import HTLgenspec. +From coqup Require HTL Verilog. +From compcert Require RTL. + +Parameter match_assocset : RTL.regset -> Verilog.assocset -> Prop. + +Inductive match_states : RTL.state -> HTL.state -> Prop := +| match_state : forall (rs : RTL.regset) assoc sf f sp rs mem m st, + match_assocset rs assoc -> + match_states (RTL.State sf f sp st rs mem) + (HTL.State m st assoc). -- cgit