avimit, I need your help on formality!!!

site:www.edaboard.com formality set svf

I have some questions about formality(rtl vs. gate(DC netlist) need your help. The Design is around 2M gate count. Thanks.
1. How to use arithmetic generator?
I have some multipler in my RTL, like:
assign c = a * b;
2. I used ”set_svf default.svf" in script, but when doing "match", formality give me a warning --"Warning: Could not process object(s) referenced in SVF (FM-340)", actually after match finished, all compare points are match except some clock gating cell (I have set "verification_clock_gate_hold_mode" to any).
When I report unmatched points with “-datapath", there are some unmatched datapath blocks（ all these blocks have multipler in their RTL, like A * B);
I am confused with these warning. can you give me a help?
thanks

formality unmatched datapath

First Question : How to use arithmetic generator?
There are two steps need to follow.
Step1 : In Dc , you need to find out ,which architecture is implemented in the optimization. report_resources -hier will give you the list of architectures.
Step2: In Formality, enable the new arithmetic generator functionality using set enable_mulitplier_generation true.
use below variable to set which architectures used for multiplier in FV.
set hdlin_multiplier_architecture Wallace. Wallace is an example , check ur DC report .

If you have multiple instances with multiple architectures, in formality you need to set it as set_architcture r:/WORK/Design/mul_1 wallace and etc....

report_architecture in formality will report you the architectures used in the design.

Second Question :
Regarding FM-340, you can ignore this Warning usually. It is mainly due to naming conventions or Differences in DC-presto parser to RTL parser in Formlaity

Best of luck ..

Regards,
Sam

Thanks Sam.
My Netlist is a flatten one. So the designware has been divided. Hot to deal with this case?
Best Regards,
Kang

Did u try the above to procedure to verify your netslist. It shodul work with Flatten netlist.

The other way to verify is 2 step process. Ask DC enginer to save an intermediate netlist before ungrouping and verify in 2 steps. step1 is RTL to Hierarchcial netlsit . step2 is Verify hierarchical netlist with Flatten netlist.

Regards,
Sam

Hi Sam,
Here is formality log :
Arch Source Instance Path
pparch svf r:/WORK/*/*/mult_403
pparch svf r:/WORK/*/*/mult_903
none N/A r:/WORK/*/*/mult_288
My concern is why the Arch of the third one is "none" and sourc is "N/A".
One more question, After verif, there are about 80 compare points are aborted,formality said that these points are too complex. these aborded points are related to a big adder, how to avoid these aborted points? That is , Can I make these points easy for formality by setting some variables?
thanks a lot

when no multipler architecture applied for r:/WORK/*/*/mult_288 using hdlin_multiplier_architecture variable it shows as none .other two mulitplers source is svf and for this multiplier source is none it shows as N/A. Need to check your svf generation.




Aborted points :
Formality stops verification after the number of failing points exceeds the 'failing_point_limit' . Default value is 20. you can set bigger number .
Unverified points are reported as aborted points and u can verify these by Incremental verification.

make sure below variable is set to high to verify complex logic.

set verification_effort_level high

verification_timeout_limit variable checks the time limit for your design verification and exits if its exceded. write small script for incremental verification automaticlally, when verification status shown as INCONCLUSIVE.

I did set verification_effort_level to high.
There isn't any failing points, but 80 aborted points.

Added after 9 minutes:

Sam,
I check my default.svf, there is a sentence for mult_903 and mult_403, but not for mult_288, like the following :
guide_multiplier -design { core_top } -instance { U_TOP_WRAPPER/U_VMCTOP/U_VIDEO/U_VID_CORE/U_VSPTOP/U_DCAC_Q_IO/U_VSPTOP_YK_KERNEL/U_QIQ_M0/mult_903 } -arch { pparch } -body { qiq_multi_DW_mult_uns_0 }
I don't know what's the reason.

Aborted points can be verified with incremental verification . Try incremental verification in Formality...

I am not sure why DC is not written out svf for your multiplier instances. Alternate solution is , using set_architecture you can pass the information to your tool.


Regards,
sam

Hello heartfree,
My questions to you.
1. What version of formality are you using
2. Has your svf annotation been 100% successfull?
2.5 You say that there are no failing points, so is your result of verification INCONCLUSIVE? or what?
3. your dc compile script, does it read hierarchial designs to make your 2M big chip. If yes, then you will have to use the svf files corresponding to each of the sub blocks.
What I suspect is that a lot of info from your svf file is missing. Remember there is also a directory that dc makes along with the .svf file which is related to the .svf file. The .svf file refreences this directory, and you cannot move your svf file from where it was generated that eaisly. Because you will have to move the directory as well. The name of this directory will be s'thing like dwsvf_*
So make sure that you collect all svf files corresponding to all sub blocks/modules/designs that your top level is consis of, then look into svf annotation carefully.
If you are using the latest formality i.e 2007_06_SP1, then in the run-log it will show how manv svf operations are 'rejected' i.e not successfully annotated.
Once you know it, then try to find why these are not annotated.
Hope it helps,
Keep writing.
Kr,
Avi
http://www.vlsiip.com

Sam and Avi, Thanks both of you. I'll provide information as much as possible for your reference.
1.The version is W-2005.03-SP1 for linux.
2. Formality printed out a warning when beginning match. the warning is :
Warning: Could not process object(s) referenced in SVF (FM-340).
After this, formality begin to generate datapath components and the log is as:
Arch Source Instance Path
pparch svf r:/WORK/*/*/mult_403
pparch svf r:/WORK/*/*/mult_903
none N/A r:/WORK/*/*/mult_288
I check the svf file, there isn't "guide_datapath" for mult_288. So there are some aborted points related
to this multiplier in final verification report.
3. Actually there is one failing points, but it was caused by inverted mapping between reference and implement,
after I removed "-", this point passed.
4.I adopted top_down method when synthesis, so there is only one svf file - default.svf. I also linked the dwsvf_*
directory in DC working directory to formality working directory.

Currently the result of verify is INCONCLUSIVE,because :
1. Some clock gate cells inserted by DC in netlist:
I have set "verification_clock_gate_hold_mode" to any.
but formality complain these clock gate cells are unmatch points. Should I constrain these clock gate cells by “set_dont_verify"???
2. Some aborted points. How to do incremental verify? After first round veriy finished, I clicked the button for "continue verify", It took formality more than 24 hours for second round verify, but these points are also aborted during verification.
These points are located in the logic which have a big adder---20 20bits-vectors is added.

1. You have taken correct step for clock gates. YOu dont have to do anything else.
2. It might be formality which is a problem. I had a hanging (inconclusive) design and I had sumbitted a ticke at solvnet. Synopsys got back to me and asked me to use a different verison of DC(yes design compiler). They recommend
DC version 2007_03_SP4.
Formality version 2007_06_SP1
When you will use the above said version of formality, you can clearly see in formality log, which of your svf commands wer rejected. and that is the key to debug the problem.
Its difficult to solve the porblem from over here I guess, as I think you have a serious issue.
One thing more if you have a hierarchial design, then try running by black boxing some of the designs, just to narrrow down the problem.
Kr,
Avi


http://www.vlsiip.com

Thanks your input.
This is my first time to use formality, you and sam gave me a lots of help on kinds of issue. Thanks a lot.
By the way, I have tried to send email to your vlsiip, but it failed. Anyways, keep in touch.