I have 2 synchronizers in my design. Formality is not able to recognize them . Formality failing points show D and stage1_sync. But stage2_sync passes.
The sample RTL code is below
reg stage1_sync, stage2_sync;
assign Q = stage2_sync;
always @(posedge CP or negedge CL) begin
if (~CL) begin
stage1_sync <= 1'b0;
stage2_sync <= 1'b0;
end else // if (~CL)
begin
stage1_sync <= D;
stage2_sync <= stage1_sync;
end
end // always @ (posedge CP)
normaly Logic Equivalent Checker tool checks two design, generally called golden & revised to be check together, so the RTL is the golden version and you need to provide the revised version, new RTL or netlist to be check logically.