( SNUG 03 Item 8 ) ----------------------------------------------- [05/14/03]
Subject: Ketchum/FormalVera/Magellan, 0-in Check & Search, Verplex BlackTie
A BREECH DELIVERY: For years I've been tracking Ketchum, the Synopsys
answer to 0-in's tool suite. Last year, Ketchum was renamed FormalVera, but
it also almost fell of my radar because no one mentioned it in last year's
SNUG survey. (See SNUG 02 #8.) It wasn't until ESNUG 394 #10, that I heard
that Ketchum wasn't dead. Anyway, Ketchum is still weakly in the game with
just a handful of users noticing. Oh, and I've heard a rumor that it's been
yet again renamed to Magellan -- you know after that guy in the early 1500s
who got lost and ended up sailing the long way around the world?
"I have some experience with 0-In's "Check" & "Search" but no extensive
experience with their formal tools."
- [ An Anon Engineer ]
"Only have experience with Verplex BlackTie, quite good. Don't know
the others."
- Tie Li of Applause Technolgy
"Ketchum? What's that? Synopsys don't appear to have been very good
at marketing this tool, and few people here have heard of it. We have
all heard of BlackTie and 0-in. 0-in appears to be the better tool,
and be further developed, but all of them suffer from only supporting
Verilog."
- [ An Anon Engineer ]
"Verplex Blacktie vs. Synopsys FormalVera (Ketchum)
My choice of Blacktie was arbitrary. When Synopsys heard I was using
the tool, they invited me to try FormalVera, which I will in future but
not for my current projects. Verplex support for Blacktie has been
excellent, also. I am reluctant to criticise the tool because my
inexperience may be the root of some of difficulties I have had. But
the problems I have experienced with Blacktie were:
- difficulty handling our bi-directional pads. In the end the
Verplex Support suggested bypassing these and working on
the internal logic only, which is what I did.
- prior to undertaking a Blacktie run, I provide an initialization
file to apply and de-assert reset. I could not find a way in
Blacktie to verify that the reset had been applied correctly, other
than to check the condition of the registers. When Blacktie
detects a failure and produces a counter example, the reset lines
are always 'X'. Does this mean a 'don't-care' condition or does it
mean an 'uninitialized' condition? It appears to me that X is used
for both don't-care and uninitialized states. I have not resolved
this with Verplex or my local CAD team. I would like to see
counter examples that use something else (e.g. '-') for don't-care
and 'X' for undefined.
- I was applying Blacktie to gate-level netlists (not RTL) and
experienced long run times (days). Having performed a long run, I
would like to be able to save the database, which couldn't be done.
Verplex Support told me that they would look to add this later.
Verplex documentation should be extended to include more examples/case
studies in applying the tool. I don't think their documentation is as
good as Synopsys for the new user."
- Alan Duffy of Motorola
|
|
