From 929ca73f8aed8c122b93527c545a38dd82d52647 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 22 Jan 2021 17:41:37 +0000 Subject: Fix imports to remove warnings when compiling --- src/hls/AssocMap.v | 6 ++++-- src/hls/HTL.v | 19 ++++++++++++++----- src/hls/HTLgen.v | 29 ++++++++++++++++++++--------- src/hls/HTLgenspec.v | 18 ++++++++++++++---- src/hls/Pipeline.v | 25 +++++++++++++++++++++---- src/hls/RTLBlockgen.v | 12 +++++------- src/hls/Veriloggen.v | 41 +++++++++++++++++++++++------------------ 7 files changed, 101 insertions(+), 49 deletions(-) (limited to 'src') diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 51afed7..1d1b77f 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -17,8 +17,10 @@ * along with this program. If not, see . *) -From vericert Require Import Vericertlib ValueInt. -From compcert Require Import Maps. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.ValueInt. Definition reg := positive. diff --git a/src/hls/HTL.v b/src/hls/HTL.v index d1c901f..c8a0041 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -17,11 +17,20 @@ * along with this program. If not, see . *) -From Coq Require Import FSets.FMapPositive. -From vericert Require Import Vericertlib ValueInt AssocMap Array. -From vericert Require Verilog. -From compcert Require Events Globalenvs Smallstep Integers Values. -From compcert Require Import Maps. +Require Import Coq.FSets.FMapPositive. + +Require compcert.common.Events. +Require compcert.common.Globalenvs. +Require compcert.common.Smallstep. +Require compcert.common.Values. +Require compcert.lib.Integers. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.Array. +Require vericert.hls.Verilog. (** The purpose of the hardware transfer language (HTL) is to create a more hardware-like layout that is still similar to the register transfer language diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 4c49828..f1e6b2a 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -17,10 +17,21 @@ * along with this program. If not, see . *) -From compcert Require Import Maps. -From compcert Require Errors Globalenvs Integers. -From compcert Require Import AST RTL. -From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad. +Require Import Coq.micromega.Lia. + +Require Import compcert.lib.Maps. +Require compcert.common.Errors. +Require compcert.common.Globalenvs. +Require compcert.lib.Integers. +Require Import compcert.common.AST. +Require Import compcert.backend.RTL. + +Require Import vericert.common.Statemonad. +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.HTL. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.Verilog. Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. @@ -557,8 +568,8 @@ Proof. rewrite PTree.gempty. congruence. (* inductive case *) intros. rewrite PTree.gsspec in H2. destruct (peq pc k). - inv H2. xomega. - apply Ple_trans with a. auto. xomega. + inv H2. unfold Ple; lia. + apply Ple_trans with a. auto. unfold Ple; lia. Qed. Lemma max_pc_wf : @@ -572,7 +583,7 @@ Proof. simplify. transitivity (Z.pos (max_pc_map m)); eauto. Qed. -Definition transf_module (f: function) : mon module := +Definition transf_module (f: function) : mon HTL.module := if stack_correct f.(fn_stacksize) then do fin <- create_reg (Some Voutput) 1; do rtrn <- create_reg (Some Voutput) 32; @@ -586,7 +597,7 @@ Definition transf_module (f: function) : mon module := match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with | left LEDATA, left LECTRL => - ret (mkmodule + ret (HTL.mkmodule f.(RTL.fn_params) current_state.(st_datapath) current_state.(st_controllogic) @@ -616,7 +627,7 @@ Definition max_state (f: function) : state := (st_datapath (init_state st)) (st_controllogic (init_state st)). -Definition transl_module (f : function) : Errors.res module := +Definition transl_module (f : function) : Errors.res HTL.module := run_mon (max_state f) (transf_module f). Definition transl_fundef := transf_partial_fundef transl_module. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 2bd1a2a..845b1d5 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -17,10 +17,20 @@ * along with this program. If not, see . *) -From compcert Require RTL Op Maps Errors. -From compcert Require Import Maps Integers. -From vericert Require Import Vericertlib Verilog ValueInt HTL HTLgen AssocMap. -Require Import Lia. +Require Import Coq.micromega.Lia. + +Require compcert.backend.RTL. +Require compcert.common.Errors. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require compcert.verilog.Op. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.Verilog. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.HTL. +Require Import vericert.hls.HTLgen. +Require Import vericert.hls.AssocMap. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. Hint Resolve Maps.PTree.elements_correct : htlspec. diff --git a/src/hls/Pipeline.v b/src/hls/Pipeline.v index ea0c32e..7f1485a 100644 --- a/src/hls/Pipeline.v +++ b/src/hls/Pipeline.v @@ -1,7 +1,24 @@ -From compcert Require Import - Maps - AST - RTL. +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020-2021 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 . + *) + +Require Import compcert.lib.Maps. +Require Import compcert.common.AST. +Require Import compcert.backend.RTL. Parameter pipeline : function -> function. diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v index 6b3e9c3..889e104 100644 --- a/src/hls/RTLBlockgen.v +++ b/src/hls/RTLBlockgen.v @@ -16,13 +16,11 @@ * along with this program. If not, see . *) -From compcert Require - RTL. -From compcert Require Import - AST - Maps. -From vericert Require Import - RTLBlock. +Require compcert.backend.RTL. +Require Import compcert.common.AST. +Require Import compcert.lib.Maps. + +Require Import vericert.hls.RTLBlock. Parameter partition : RTL.function -> Errors.res function. diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index a0be0fa..80c0669 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -16,10 +16,15 @@ * along with this program. If not, see . *) -From compcert Require Import Maps. -From compcert Require Errors. -From compcert Require Import AST. -From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt. +Require Import compcert.common.AST. +Require compcert.common.Errors. +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.AssocMap. +Require Import vericert.hls.HTL. +Require Import vericert.hls.ValueInt. +Require Import vericert.hls.Verilog. Definition transl_list_fun (a : node * Verilog.stmnt) := let (n, stmnt) := a in @@ -41,23 +46,23 @@ Definition transl_module (m : HTL.module) : Verilog.module := let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in let body := - Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1))) - (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint)))) - (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) - :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) + Valways (Vposedge m.(HTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(HTL.mod_reset)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint)))) + (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.mod_st)) case_el_data (Some Vskip)) :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in - Verilog.mkmodule m.(mod_start) - m.(mod_reset) - m.(mod_clk) - m.(mod_finish) - m.(mod_return) - m.(mod_st) - m.(mod_stk) - m.(mod_stk_len) - m.(mod_params) + Verilog.mkmodule m.(HTL.mod_start) + m.(HTL.mod_reset) + m.(HTL.mod_clk) + m.(HTL.mod_finish) + m.(HTL.mod_return) + m.(HTL.mod_st) + m.(HTL.mod_stk) + m.(HTL.mod_stk_len) + m.(HTL.mod_params) body - m.(mod_entrypoint). + m.(HTL.mod_entrypoint). Definition transl_fundef := transf_fundef transl_module. -- cgit