diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 17:41:37 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-22 17:41:37 +0000 |
| commit | 929ca73f8aed8c122b93527c545a38dd82d52647 (patch) | |
| tree | 58ef9d724a3aa15d849563941deae5fe89f78a3f /src/hls/HTLgen.v | |
| parent | 6370fff13320a70c852c3faa78f17dadbfb1aeb8 (diff) | |
| download | vericert-929ca73f8aed8c122b93527c545a38dd82d52647.tar.gz vericert-929ca73f8aed8c122b93527c545a38dd82d52647.zip | |
Fix imports to remove warnings when compiling
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 29 |
1 files changed, 20 insertions, 9 deletions
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 <https://www.gnu.org/licenses/>. *) -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. |