From 178a7c4781c96857fe0a33c777da83e769516152 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 11 Jul 2021 15:59:21 +0200 Subject: Remove unnecessary files and proofs --- src/Compiler.v | 4 ++-- src/extraction/Extraction.v | 8 ++++---- src/hls/HTLPargen.v | 5 +++-- src/hls/RTLBlockInstr.v | 6 +++--- src/hls/RTLPargen.v | 7 ++++--- src/hls/RTLPargenproof.v | 3 ++- 6 files changed, 18 insertions(+), 15 deletions(-) (limited to 'src') diff --git a/src/Compiler.v b/src/Compiler.v index 268f451..de29889 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -216,7 +216,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := (* This is an unverified version of transf_hls with some experimental additions such as scheduling that aren't completed yet. *) -Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := +(*Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@ -245,7 +245,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@@ RTLPargen.transl_program @@@ HTLPargen.transl_program @@ print print_HTL - @@ Veriloggen.transl_program. + @@ Veriloggen.transl_program.*) (*| Correctness Proof diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 00a1f00..6abe4e0 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -179,7 +179,7 @@ Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". Extract Constant Pipeline.pipeline => "SoftwarePipelining.pipeline". Extract Constant RTLBlockgen.partition => "Partition.partition". -Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". +(*Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".*) (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -187,11 +187,11 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction Verilog.module vericert.Compiler.transf_hls - vericert.Compiler.transf_hls_temp - RTLBlockgen.transl_program RTLBlockInstr.successors_instr +(* vericert.Compiler.transf_hls_temp*) +(* RTLBlockgen.transl_program RTLBlockInstr.successors_instr*) HTLgen.tbl_to_case_expr Pipeline.pipeline - RTLBlockInstr.sat_pred_temp +(* RTLBlockInstr.sat_pred_temp*) Verilog.stmnt_to_list Compiler.transf_c_program Compiler.transf_cminor_program diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index eda597a..9e1f156 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -643,7 +643,7 @@ Definition add_control_instr_force_state_incr : (AssocMap.set n st s.(st_controllogic))). Abort. -Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := +(*Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := fun s => OK tt (mkstate s.(st_st) @@ -708,7 +708,7 @@ Lemma create_new_state_state_incr: s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). -Admitted. +Abort. Definition create_new_state (p: node): mon node := fun s => OK s.(st_freshstate) @@ -876,3 +876,4 @@ Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program : if main_is_internal p then transform_partial_program transl_fundef p else Errors.Error (Errors.msg "Main function is not Internal."). +*) diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 86f8eba..5e123a3 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -211,9 +211,9 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : - apply orb_true_intro. apply satFormula_mult2 in H. inv H. apply i in H0. auto. apply i0 in H0. auto. -Admitted. +Abort. -Definition sat_pred (bound: nat) (p: pred_op) : +(*Definition sat_pred (bound: nat) (p: pred_op) : option ({al : alist | sat_predicate p (interp_alist al) = true} + {forall a : asgn, sat_predicate p a = false}). refine @@ -243,7 +243,7 @@ Definition sat_pred_temp (bound: nat) (p: pred_op) := match trans_pred_temp bound p with | Some fm => boundedSatSimple bound fm | None => None - end. + end.*) Inductive instr : Type := | RBnop : instr diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index e2e9a90..5ad3f90 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -473,9 +473,9 @@ Lemma sems_det: forall v v' mv mv', (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\ (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv'). -Proof. Admitted. +Proof. Abort. -Lemma sem_value_det: +(*Lemma sem_value_det: forall A ge tge sp st f v v', ge_preserved ge tge -> sem_value A ge sp st f v -> @@ -657,7 +657,7 @@ Lemma abstract_execution_correct: RTLBlock.step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') -> exists rs'', RTLPar.step_instr_block tge sp (InstrState rs m) bb' (InstrState rs'' m') /\ regs_lessdef rs' rs''. -Proof. Admitted. +Proof. Abort. (*| Top-level functions @@ -689,3 +689,4 @@ Definition transl_fundef := transf_partial_fundef transl_function_temp. Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := transform_partial_program transl_fundef p. +*) diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index eb7931e..a0c01fa 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -16,7 +16,7 @@ * along with this program. If not, see . *) -Require Import compcert.backend.Registers. +(*Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Errors. Require Import compcert.common.Linking. @@ -286,3 +286,4 @@ Section CORRECTNESS. Qed.*) End CORRECTNESS. +*) -- cgit