Formal verification of a clock-gated netlist with Formality

Status
Not open for further replies.

kyhcj21

Newbie level 1
Joined
Oct 12, 2009
Messages
1
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Location
South Korea
Visit site
Activity points
1,291
Hi, I've created my own clock gating method, and I'm trying to check the logic equivalence by using Synopsys Formality. However, verification always fails even though I've checked the functional equivalence by RTL simulation. Also, I've set the set_clock_gate_hold_mode to 'any'.

My clock gating method is as follows:

1. Create an enable signal with two pulses (start/done). When 'start' pulse is on, the enable signal asserts to 1 and holds the value until 'done' arises.

2. Apply latch-based clock gating with the enable signal created above.


I've analyzed the input patterns of failing verifications, and found out that there are cases when the clock input of reference's DFF is 1 and the clock input of implementation's DFF is 0. These cases show that Formality does not account for my clock gating logic. Is there any way I can successfully verify my logic?

Thanks in advance.
 

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