From d460696e02f02ae25752678652757da11a44f50a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 22 Jan 2021 22:25:06 +0000 Subject: Add match_states for RTLPargen proof --- src/hls/HTLgenproof.v | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) (limited to 'src/hls/HTLgenproof.v') 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 . *) -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. -- cgit