diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:10:22 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:10:22 +0100 |
| commit | f6569b736d4ded08a011f55bd6001c89e899fd5c (patch) | |
| tree | cc76bb6b36dc7cfc2fc5fc2b216c5b1cde0ab752 | |
| parent | 86e64fd05cea7b1da996701cd3653db5f471f8d1 (diff) | |
| download | vericert-f6569b736d4ded08a011f55bd6001c89e899fd5c.tar.gz vericert-f6569b736d4ded08a011f55bd6001c89e899fd5c.zip | |
Add comments next to admitted theorems
| -rw-r--r-- | src/hls/ClockRegisters.v | 2 | ||||
| -rw-r--r-- | src/hls/DVeriloggenproof.v | 2 | ||||
| -rw-r--r-- | src/hls/HTLPargen.v | 8 |
3 files changed, 6 insertions, 6 deletions
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 |