aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/ClockRegisters.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/hls/ClockRegisters.v')
-rw-r--r--src/hls/ClockRegisters.v2
1 files changed, 1 insertions, 1 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).