Continue to Site

Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronics Discussion Forum focused on EDA software, circuits, schematics, books, theory, papers, asic, pld, 8051, DSP, Network, RF, Analog Design, PCB, Service Manuals... and a whole lot more! To participate you need to register. Registration is free. Click here to register now.

Formal verification of a clock-gated netlist with Formality

Status
Not open for further replies.

kyhcj21

Newbie level 1
Newbie level 1
Joined
Oct 12, 2009
Messages
1
Helped
0
Reputation
0
Reaction score
0
Trophy points
1,281
Location
South Korea
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.

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Back
Top