Formality - Synchronizers causing a problem

[manchuk]

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)

Thanks

 

[rca]

eh, your code seems correct. I believe you provide a second input to formality to check versus this code ?

 

[manchuk]

@rca : I am quite new to formality. How can we provide the second input to formality ?

 

[rca]

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.