From 43b5e109f3528cb689a0e3d32091370405d43715 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 12 Feb 2025 17:45:02 +0100 Subject: [PATCH] formalff: Document -declockgate option --- passes/sat/formalff.cc | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index 3ebae4bc4ca..a04ab064c1e 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -538,6 +538,12 @@ struct FormalFfPass : public Pass { log(" Add assumptions that constrain wires with the 'replaced_by_gclk'\n"); log(" attribute to the value they would have before an active clock edge.\n"); log("\n"); + log(" -declockgate\n"); + log(" Detect clock-gating patterns and modify any FFs clocked by the gated\n"); + log(" clock to use the ungated clock with the gate signal as clock enable.\n"); + log(" This doesn't affect the design's behavior during FV but can enable the\n"); + log(" use of formal verification methods that only support a single global\n"); + log(" clock.\n"); // TODO: An option to check whether all FFs use the same clock before changing it to the global clock }