( ESNUG 400 Item 15 ) -------------------------------------------- [10/10/02]
From: Steve Golson <sgolson@trilobyte.com>
Subject: Golson's Comparison Of Formality vs. Chrysalis Design VERIFYer
Hi, John,
I've been using formal verification for about a year to verify some very
extensive ECOs being made to a multi-million gate netlist. (More on that
later; I plan on writing a SNUG paper about the methodology.)
We started out using Chrysalis Design VERIFYer, which was subsequently
acquired by Avanti and recently by Synopsys. I was able to use Synopsys' own
formal verification tool Formality to re-run some of this work. What follows
is a summary of my experience with the two tools. I've got some critical
comparisons, and some suggestions for improvements.
I used many versions of Design VERIFYer; most recently all my work has been
with the current version v2001.3.
All my Formality work has been with 2002.05.
1. Formality has much easier setup than Design VERIFYer. The GUI and "flow"
methodology was pretty intuitive and made it easy to get started.
(Caveat: it probably helped that I was already an experienced Design VERIFYer
user, and understood a lot of the fundamental issues with equivalence
checking.)
2. Formality has a *much* nicer schematic display. It looks similar to
Design Vision.
3. Formality has nicer Tcl scripting.
4. Formality matching uses syntax stolen from "sed" which allows you to
easily try it out before running the tool (and without consuming a license).
Nice!
5. Design VERIFYer schematic window splits vertically as well as
horizontally. Also there are buttons to turn off each A/B view
independently. Very nice when you are just poking around in one netlist.
6. In the Formality schematic, when you roll over an object, the pin name
should appear. (And when you click on it.)
7. When Formality shows a failing pattern, it doesn't do a very good job
showing equivalent nets. You need to show the mapping somehow. Design
VERIFYer does a good job displaying all the logically equivalent names for a
signal.
8. Formality set_equivalence should work on pins. Also need to allow
set_invert on pins and nets. I suppose I should just use
create_cutpoint_blackbox and turn all my pins into ports.
9. In Formality when you click the GUI button "3. Setup" button, you aren't
automatically in Setup mode. At first I thought this was a bug, but now I'm
convinced it's a feature. Here's a great explanation from a Formality
specialist at Synopsys:
This is designed to save new users (or harried experienced users, or user
who are just dumb as posts like me) from themselves. One of the really
nice things about Formality is that it allows the user to iterate through
the major steps without repeating a lot of computation. The best example
is the compare point matching stage. If Formality were unable to fully
match the designs and you needed to give it help, then after giving it that
help once you hit the run matching button the tool will only operate on the
subset of points that were unmatched.
The way Formality used to work and the way I think Design VERIFYer works
today, if you need to give the tool some help once you matched again the
tool would start the entire matching process from scratch. A waste of CPU
cycles for one thing. In some cases people got in trouble that way. Let's
say they were not as good with SED as they thought they were. The SED rule
they applied may have farther reaching affects than planned and caused some
points to misalign. The odds of that are greatly reduced if the rule only
impacts the subset of unmatched points. Another great benefit is that it
allows for optional automatic matching techniques to be applied with
greater success (greatly minimizing the need to ever write a SED rule).
There is an optional algorithm that matches based on the best subset set of
a name. Sometimes the best subset match is not the right match (that is
why it is optional). With the iterative approach this can be turned on
after the first matching has been attempted, therefor it is only working on
the subset of unmatched points, thus greatly improving the odds that the
best match is the right match.
OK so iterative matching is a cool thing, what does that have to do with
the setup button that won't put me in setup mode? Well, changing setup
variables changes the ground rules for matching, making the matching
results invalid. If you revert to setup mode we have to dump the matching
data and start from scratch again. Since you are throwing away good work
we want to be sure that is really what you want to do. Sometimes people
want to go to the setup screen just to check on the setup variables, not to
change them. By making you forcibly put us in set up mode (by typing setup
or punching the "revert to setup" button on the setup screen) we allow you
check without throwing away the matching info. Make sense? In a flow where
you end up going back to setup to change things this seems a bit clunky at
first, but it enables us to implement iterative steps that greatly
facilitate verification in the normal flow of things.
Did I use the word greatly enough in that explanation?
10. Formality sometimes takes several minutes to exit after the
"Thank you for using Formality (R)!"
message. This is weird. I can't figure out what it's doing. Formality
generates a work area and deletes it after its finished (the FM_WORK
subdirectory) so maybe that's what is going on. Very strange.
11. Formality uses signature analysis to help figure out signals that match
in the two netlists. This is cool! It can make matching very simple, as you
don't have to specify every little flop equivalence.
12. When Formality shows failing sim patterns, it should show the pin name as
well as the instance name. Sometimes it's QN rather than Q, and having the
pin name makes it much easier to understand what's going on.
13. Design VERIFYer displays a *VERY* nice comparison of internal nets in rtl
mode! For example, here's a snippet from a Design VERIFYer log_verify file:
Equivalence #3787 - The two groups are equivalent.
-> NSB +1 17258 A.$371
+1 17258 A.make_it_idle
+1 5324 B.n15216
-1 13346 B.n15221
-1 13346 B.X14130.Z
-> NSB +1 5324 B.X14251.Z
So now I know that my internal rtl signal "make_it_idle" appears on netlist
wire "n15216" and an inverted version on "n15221". This is great when you
are trying to hack in a gate-level ECO.
Formality doesn't seem to do this (at least I never figured out how).
Perhaps this is because VERIFYer often splits logic cones on non-state point
boundaries (NSB) while Formality mostly uses state points (i.e. flops). From
the Design VERIFYer manual:
Non-State Boundaries (NSBs) are intermediate pseudo-statepoints that are
occasionally used within a logic cone to help manage comparisons between
usually large logic cones.
My Synopsys specialist tells me:
On the topic of splitting things on non-state boundaries, Formality can do
that also. It happens under the hood sometimes for the same reason noted
in the Design VERIFYer manual (making large cones more manageable). As the
user you can also insert this points in the cone if you want to. What you
are doing is inserting a single input/single output black box in the logic
cone (create_cutpoint_blackbox is the command if memory serves). Perhaps
there is some additional reporting we can do in cases where we have done
this under the hood and therefor know something about the equivalence (or
non equivalence) of the various subcones.
It would be interesting to see if Design VERIFYer splits things into more
NSBs than Formality (i.e. does Formality tend to have larger logic cones).
14. Design VERIFYer requires separate "build" and "verify" steps. This
requires two different licenses (normally you get one of each). This allows
you to parallelize your work (you can build on one machine while you compare
on another). Very nice.
15. Formality allows you to quickly and easily check just one output, and
ignore all the rest. You can do this in Design VERIFYer, but it's painful.
16. Formality can read synthesis .db libraries directly, while Design
VERIFYer has to read your sim models. This adds some time and complexity to
the Design VERIFYer runs. "But wait!" you say. What if there is a bug in
the synth library? Well, simply do a comparison of the two libraries first,
then you know that both representations are equivalent. Or you can always
have Formality read the sim libs rather than the .db library. (Reading cell
models on demand can sometimes be more efficient than read in the whole lib
as you have to do with .db libs.) Formality has this cool "-vcs" option where
it can use the same command-line syntax as VCS for specifying files,
libraries, directories, etc.
This brings me to the old canard "Formality shares code with Design
Compiler". Maybe this was true a long time ago (back when the earth was
still cooling), but is no more. The *important* and *critical* code is
separate. Separate development, separate people.
Nevertheless I think that it is a *good* thing if *some* of the code is the
same: I like having the schematic display look like Design Vision, for
example. Also being able to read .db files is great. (The paranoid among us
can do a library verification against your sim models to be sure.)
Finally, here's a head-to-head comparison of both tools on a variety of
netlists. These are all gate-to-gate equivalence checks.
All runs were done with 32-bit executables under Solaris 8 running on a
750MHz Sun Blade 1000. The CPU time for Design VERIFYer is the sum of the
two build runs plus the verify run.
The following designs are all structurally identical. Design VERIFYer's
name-based compare mode was used. Even for rather large designs the runs
only take a few minutes. Design VERIFYer is consistently faster than
Formality, and also requires less memory. It appears that Design VERIFYer's
name-based algorithm is much more efficient than Formality's algorithm.
DV = Design VERIFYer
FM = Formality
CPU time memory swap
(hours) (Mbytes) (Mbytes)
Design Cells Flops DV FM DV FM DV FM
--------------------------------------------------------------
M5 100143 20261 0.1 0.2 411 938 449 964
M8 89507 13128 0.1 0.2 339 897 380 923
M9 86373 13989 0.1 0.2 369 1105 409 1131
M11 81557 11798 0.1 0.2 291 1116 314 1142
M12 75459 11751 0.1 0.1 261 896 291 921
M14 73636 7745 0.1 0.2 245 1076 273 1101
M18 58860 6891 0.1 0.1 223 879 263 904
M20 46704 10065 0.1 0.1 195 865 235 890
M21 46704 10065 0.1 0.2 202 1055 243 1080
M24 38041 6224 0.1 0.1 174 868 214 893
M26 35213 5111 0.1 0.1 155 859 196 884
M27 32116 5804 0.1 0.2 242 1064 252 1090
M28 31356 6422 0.1 0.1 160 858 201 883
M29 31258 5859 0.1 0.1 155 858 196 883
M34 27740 4120 0.0 0.2 76 1047 86 1072
M35 26894 5033 0.0 0.1 120 859 131 883
M39 26558 3079 0.1 0.1 169 1047 179 1072
M40 25834 2913 0.0 0.1 92 1047 102 1072
M41 25260 4146 0.1 0.1 130 1047 170 1072
M44 20754 4455 0.0 0.1 100 859 110 884
M45 20221 4877 0.0 0.1 71 1047 81 1072
M46 17341 3083 0.0 0.1 67 1048 77 1073
M47 16914 1259 0.0 0.1 53 1048 64 1073
M48 15467 2979 0.0 0.1 16 859 27 884
M49 15056 2977 0.0 0.1 69 859 79 884
M50 15056 2977 0.0 0.1 80 859 91 884
M51 11674 1783 0.0 0.1 16 859 27 884
M52 9767 1143 0.0 0.1 48 1048 58 1073
M53 7019 1293 0.0 0.1 16 859 27 884
M55 4330 864 0.0 0.1 29 1048 39 1073
M56 4189 575 0.0 0.1 16 860 27 884
M57 2883 388 0.0 0.1 16 860 27 884
M58 2529 428 0.0 0.1 16 1048 27 1073
M60 1178 205 0.0 0.1 16 1048 27 1073
M61 517 0 0.0 0.1 16 859 27 884
M62 510 0 0.0 0.1 16 1048 27 1073
M63 343 0 0.0 0.1 16 1048 27 1073
The following designs are structurally different, requiring much more
computation. Design VERIFYer was run in "rtl" mode.
CPU time memory swap
(hours) (Mbytes) (Mbytes)
Design Cells Flops DV FM DV FM DV FM
--------------------------------------------------------------
M1 1282859 165728 --- 3.9 -- 2287 -- 2622
M2 1026971 157077 --- 1.4 -- 1670 -- 1819
M3 108025 16890 202.2* 0.6 1036 1286 1088 1315
M4 104761 10388 3.0 0.3 1153 1188 1192 1216
M6 91340 7403 12.9 0.4 1132 1073 1170 1105
M7 90412 13862 19.5 1.0 1259 1178 1303 1207
M10 84832 9167 0.8 0.2 943 1152 983 1181
M13 73829 5920 0.2 0.2 445 1123 485 1148
M15 71201 9339 3.8 0.2 611 917 651 943
M16 66820 5927 3.7 0.3 1021 1254 1058 1283
M17 64583 7592 4.9 0.1 828 883 867 908
M19 47202 7346 0.1 0.2 297 1060 335 1085
M22 43428 6569 0.2 0.2 392 1058 432 1083
M23 38342 5785 1.0 0.2 1241 1068 1281 1093
M25 35337 4748 2.9 0.5 736 1126 775 1154
M30 30390 2811 0.2 0.1 233 898 272 922
M31 29165 4298 0.4 0.2 356 867 394 892
M32 28405 5275 0.1 0.1 262 887 300 912
M33 28281 3911 0.6 0.2 348 920 387 946
M36 26878 2652 1.1 0.2 986 1047 1025 1072
M37 26780 0 --- 0.6 -- 1145 -- 1174
M38 26780 0 --- 0.7 -- 1145 -- 1174
M42 21116 3833 0.1 0.1 268 860 307 884
M43 20768 2967 0.1 0.1 146 859 187 884
M54 5912 729 0.0 0.1 17 859 27 884
M59 1423 393 0.0 0.1 16 1048 27 1073
* Design M3 did not successfully complete when run under Design VERIFYer
(some endpoints had "timeouts"). I was unable to resolve this problem. Note
that Formality was able to complete this design in under an hour.
Designs M37 and M38 never completed when run under Design VERIFYer (I killed
it after 531 hours). Designs M1 and M2 were not attempted under Design
VERIFYer.
However Formality had no problem with any of the designs, even the largest
which has over 1.2 million instances. The Formality run time is much much
less than Design VERIFYer, with all runs (except the largest) taking under an
hour.
In short, Formality capacity is outstanding. It handles multi-million gate
designs with ease.
Memory usage is similar betweeen the two tools.
Notice that the size of the design (number of cells, number of flops) is
*not* a perfect predictor of how long the run will take. As always, your
mileage may vary. The underlying complexity of the design has a huge impact
on the ability of the tool to successfully complete.
My hope is that now that Synopsys owns both Design VERIFYer and Formality,
the strengths of each will be combined into one really outstanding formal
verification tool.
- Steve Golson
Trilobyte Systems Carlisle, MA
============================================================================
Trying to figure out a Synopsys bug? Want to hear how 14,488 other users
dealt with it? Then join the E-Mail Synopsys Users Group (ESNUG)!
!!! "It's not a BUG, jcooley@TheWorld.com
/o o\ / it's a FEATURE!" (508) 429-4357
( > )
\ - / - John Cooley, EDA & ASIC Design Consultant in Synopsys,
_] [_ Verilog, VHDL and numerous Design Methodologies.
Holliston Poor Farm, P.O. Box 6222, Holliston, MA 01746-6222
Legal Disclaimer: "As always, anything said here is only opinion."
The complete, searchable ESNUG Archive Site is at http://www.DeepChip.com
|
|
