Formality - Synchronizers causing a problem

Status
Not open for further replies.

manchuk

Newbie level 5
Joined
Jan 17, 2008
Messages
10
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Location
Portland
Activity points
1,364
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
 

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

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

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.
 

Status
Not open for further replies.
Cookies are required to use this site. You must accept them to continue using the site. Learn more…