From f6569b736d4ded08a011f55bd6001c89e899fd5c Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 10 Aug 2023 12:10:22 +0100
Subject: Add comments next to admitted theorems

---
 src/hls/ClockRegisters.v   | 2 +-
 src/hls/DVeriloggenproof.v | 2 +-
 src/hls/HTLPargen.v        | 8 ++++----
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/hls/ClockRegisters.v b/src/hls/ClockRegisters.v
index 4b1c37a..fee89fb 100644
--- a/src/hls/ClockRegisters.v
+++ b/src/hls/ClockRegisters.v
@@ -234,7 +234,7 @@ Program Definition transf_module (m: DHTL.module) : option DHTL.module :=
   | _ => None
   end.
 Next Obligation.
-Admitted.
+Admitted. (* This translation pass is only used for testing. *)
 
 Definition transl_module (m : DHTL.module) : Errors.res DHTL.module :=
   Verilog.handle_opt (Errors.msg "ClockRegisters: not translated") (transf_module m).
diff --git a/src/hls/DVeriloggenproof.v b/src/hls/DVeriloggenproof.v
index 31cdfca..197d9a6 100644
--- a/src/hls/DVeriloggenproof.v
+++ b/src/hls/DVeriloggenproof.v
@@ -501,7 +501,7 @@ Section CORRECTNESS.
   (*     repeat rewrite_eq. apply match_state. assumption. *)
   (*   - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. *)
   (*     repeat rewrite_eq. apply match_state. assumption. *)
-  (* Qed. *) Admitted.
+  (* Qed. *) Admitted. (* This translation pass is only used for testing. *)
   #[local] Hint Resolve transl_step_correct : verilogproof.
 
   Lemma transl_initial_states :
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 1bc0fd5..e493989 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -155,7 +155,7 @@ Lemma declare_reg_state_incr :
        (AssocMap.set r (i, VScalar sz) s.(st_scldecls))
        s.(st_arrdecls)
        s.(st_datapath)).
-Proof. Admitted.
+Proof. Admitted. (* This translation pass is only used for testing. *)
 
 Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit :=
   fun s => OK tt (mkstate
@@ -177,7 +177,7 @@ Lemma declare_arr_state_incr :
        s.(st_scldecls)
        (AssocMap.set r (i, VArray sz ln) s.(st_arrdecls))
        s.(st_datapath)).
-Proof. Admitted.
+Proof. Admitted. (* This translation pass is only used for testing. *)
 
 Definition declare_arr (i : option io) (r : reg) (sz : nat) (ln : nat) : mon unit :=
   fun s => OK tt (mkstate
@@ -479,8 +479,8 @@ Program Definition transf_seq_blockM (fin rtrn stack preg: reg) (ni: node * ParB
     | Errors.Error m => Error m
     end.
 Next Obligation.
-admit.
-Admitted.
+admit. (* This translation pass is only used for testing. *)
+Admitted. (* This translation pass is only used for testing. *)
 
 Definition declare_regs (i: instr): mon unit :=
   match i with
-- 
cgit