https://www.reddit.com/r/chipdesign/comments/kv2ebv/glitches_in_clock_gating_cell/

clock_gate_post_control.v

// Credit : https://github.com/YosysHQ/yosys-bigsim/blob/master/openmsp430/rtl/omsp_clock_gate.v
//----------------------------------------------------------------------------
// Copyright (C) 2009 , Olivier Girard
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions
// are met:
//     * Redistributions of source code must retain the above copyright
//       notice, this list of conditions and the following disclaimer.
//     * Redistributions in binary form must reproduce the above copyright
//       notice, this list of conditions and the following disclaimer in the
//       documentation and/or other materials provided with the distribution.
//     * Neither the name of the authors nor the names of its contributors
//       may be used to endorse or promote products derived from this software
//       without specific prior written permission.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY,
// OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF
// THE POSSIBILITY OF SUCH DAMAGE
//
//----------------------------------------------------------------------------
//
// *File Name: omsp_clock_gate.v
// 
// *Module Description:
//                       Generic clock gate cell for the openMSP430
//
// *Author(s):
//              - Olivier Girard,    olgirard@gmail.com
//
//----------------------------------------------------------------------------
// $Rev: 103 $
// $LastChangedBy: olivier.girard $
// $LastChangedDate: 2011-03-05 15:44:48 +0100 (Sat, 05 Mar 2011) $
//----------------------------------------------------------------------------

module  clock_gating_post_control (

// OUTPUTs
    gclk,                      // Gated clock

// INPUTs
    clk,                       // Clock
    enable,                    // Clock enable
    scan_enable                // Scan enable (active during scan shifting)
);

// OUTPUTs
//=========
output         gclk;           // Gated clock

// INPUTs
//=========
input          clk;            // Clock
input          enable;         // Clock enable
input          scan_enable;    // Scan enable (active during scan shifting)


//=============================================================================
// CLOCK GATE: LATCH + AND
//=============================================================================
   
// Enable clock gate during scan shift
// (the gate itself is checked with the scan capture cycle)
wire    enable_in =   (enable_latch | scan_enable);

// LATCH the enable signal
reg     enable_latch;
always @(clk or enable)
  if (~clk)
    enable_latch <= enable;

// AND gate
assign  gclk      =  (clk & enable_in);

`ifdef FORMAL
reg first_clock_had_passed;
initial first_clock_had_passed = 0;
always @($global_clock) first_clock_had_passed <= 1;

initial assume(clk == 1);

always @($global_clock)
begin
	if(first_clock_had_passed)
		assume(clk == ~$past(clk));
end

always @($global_clock)
	assume(enable == 0);

localparam MAX_LIMIT = 16;
reg [$clog2(MAX_LIMIT)-1:0] count;
initial count = 0;

always @(posedge clk)
begin
	count <= count + 1;
end

localparam STARTS_FALLING = 4;
localparam STARTS_RISING = 8;

always @($global_clock)
begin
	// scan_enable signal is asserted low for (STARTS_RISING-STARTS_FALLING-1) clock cycles
	if((count > STARTS_FALLING) && (count < STARTS_RISING))  
		assume(scan_enable == 0);
		
	else
		assume(scan_enable == 1);
end

always @($global_clock)
begin
	if(first_clock_had_passed)
		cover(~gclk && $past(gclk));
end

always @($global_clock) if (!$rose(clk)) assume($stable(enable));
always @($global_clock) if (!$rose(clk)) assume($stable(scan_enable));
`endif

endmodule // clock_gating_post_control

clock_gate_pre_control.v

// Credit : https://github.com/YosysHQ/yosys-bigsim/blob/master/openmsp430/rtl/omsp_clock_gate.v
//----------------------------------------------------------------------------
// Copyright (C) 2009 , Olivier Girard
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions
// are met:
//     * Redistributions of source code must retain the above copyright
//       notice, this list of conditions and the following disclaimer.
//     * Redistributions in binary form must reproduce the above copyright
//       notice, this list of conditions and the following disclaimer in the
//       documentation and/or other materials provided with the distribution.
//     * Neither the name of the authors nor the names of its contributors
//       may be used to endorse or promote products derived from this software
//       without specific prior written permission.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
// AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
// IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
// ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
// LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY,
// OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
// SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
// INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
// CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
// ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF
// THE POSSIBILITY OF SUCH DAMAGE
//
//----------------------------------------------------------------------------
//
// *File Name: omsp_clock_gate.v
// 
// *Module Description:
//                       Generic clock gate cell for the openMSP430
//
// *Author(s):
//              - Olivier Girard,    olgirard@gmail.com
//
//----------------------------------------------------------------------------
// $Rev: 103 $
// $LastChangedBy: olivier.girard $
// $LastChangedDate: 2011-03-05 15:44:48 +0100 (Sat, 05 Mar 2011) $
//----------------------------------------------------------------------------

module  clock_gate_pre_control (

// OUTPUTs
    gclk,                      // Gated clock

// INPUTs
    clk,                       // Clock
    enable,                    // Clock enable
    scan_enable                // Scan enable (active during scan shifting)
);

// OUTPUTs
//=========
output         gclk;           // Gated clock

// INPUTs
//=========
input          clk;            // Clock
input          enable;         // Clock enable
input          scan_enable;    // Scan enable (active during scan shifting)


//=============================================================================
// CLOCK GATE: LATCH + AND
//=============================================================================
   
// Enable clock gate during scan shift
// (the gate itself is checked with the scan capture cycle)
wire    enable_in =   (enable | scan_enable);

// LATCH the enable signal
reg     enable_latch;
always @(clk or enable_in)
  if (~clk)
    enable_latch <= enable_in;

// AND gate
assign  gclk      =  (clk & enable_latch);


endmodule // clock_gate_pre_control

clock_gating_post_control.sby

[tasks]
proof
cover

[options]
proof: mode prove
proof: depth 10

cover: mode cover
cover: depth 40
cover: append 20

multiclock on

[engines]
smtbmc yices
# smtbmc boolector
# abc pdr
# aiger avy
# aiger suprove

[script]
read_verilog -formal -sv clock_gating_post_control.v

prep -top clock_gating_post_control

[files]
clock_gating_post_control.v

clock_gating_post_control.ys

# read design
read_verilog clock_gate_post_control.v
hierarchy -check

# high-level synthesis
proc; opt; fsm; opt; memory; opt

# low-level synthesis
techmap; opt
show

clock_gating_pre_control.ys

# read design
read_verilog clock_gate_pre_control.v
hierarchy -check

# high-level synthesis
proc; opt; fsm; opt; memory; opt

# low-level synthesis
techmap; opt
show