( ESNUG 382 Item 2 ) -------------------------------------------- [11/15/01]

Subject: ( ESNUG 381 #6 ) Verplex LTX/LEC, Circuit Semantics Inc, Prolific

> We are trying to verify our standard cells by ensuring that vendor
> provided Verilog models are equivalent to the SPICE netlist.  Using Tuxedo
> LTX, we tried extracting a Verilog model from the SPICE netlist and then
> verifing equivalency between the extracted Verilog model and golden
> Verilog model by running Verplex LEC.  This flow failed to detect a
> previously known dynamic glitch caused by a pass transisitor in one of
> the standard flops.  It appears that the only way to detect this kind of
> glitch is through SPICE simulation.  I would like to know if there's an
> automated way to generate exhaustive input stimulus to verify
> functionality of sequential cells.
>
>     - Dhruba Kalita
>       Intel


From: Howard Landman <howard.landman@vitesse.com>

Hi, John,

In theory Dhruba would have to try all possible transition combinations (and
for SPICE, vary the relative timing of the changing signals as well.)  There
are 2^n combinational input vectors for an n-input cell, so to look at all
possible transitions requires (2^n)*(2^n) = 2^(2*n) vectors.  For a 6-input
cell that's 4K vectors, and it goes up by a factor of 4 for each additional
input.

But even that doesn't handle things like setup and hold time, which typically
are done by binary splitting searches.  For each logic state for which you
want to get setup or hold info, such a search will take k simulations, where
k is the number of bits of accuracy you want in your result.  (Assuming you
do it the standard naive way, see discussion below.)

There are companies which sell cell characterization software, such as
Circuit Semantics, Inc. (http://www.circuitsemantics.com), that claim to
handle all this automatically.  We've had fairly good results with CSI's
software - there are some knobs that need to be set carefully and there are
some problems with generated Verilog models, but overall it seems to work.
Other companies with related products or services include:

	Prolific, Inc. (http://www.prolificinc.com)
	APT Software (http://www.aptsoftware.com)
	Silicon Metrics (http://www.siliconmetrics.com)
	Library Technologies (http://www.libtech.com)
	Z Circuit Automation (http://www.z-circuit.com)

I think Compass had something in this area too, but I don't know what's
become of it.

None of the characterization software I've seen has handled the subtle
tradeoff between setup, hold, and clk-to-Q delay in a way I would consider
correct.  Partly, this is a function of .lib format, which I feel is
fundamentally broken in this regard.  If you do a 3-D plot of setup, hold,
and clk-to-Q for any given FF you will see that they trade off against each
other in roughly hyperbolic fashion.  Most systems characterize setup at
infinite hold, and characterize hold at infinite setup, and then guardband
them using some fudge factor.  But it's possible for that process to arrive
at setup and hold numbers such that, if you just barely meet the setup time
and just barely meet the hold time, the FF doesn't work!  Plus, as you
approach the minimum setup or hold, the clk-to-Q delay increases.  The .lib
format has no mechanism for expressing any of these tradeoffs, even if you
gather all the needed data.  That forces the guardbanding to be unnecessarily
large, which in turn reduces the accuracy of timing analysis and synthesis.

    - Howard Landman
      Vitesse Semiconductor                      Longmont, CO


 Sign up for the DeepChip newsletter.
Email
 Read what EDA tool users really think.


Feedback About Wiretaps ESNUGs SIGN UP! Downloads Trip Reports Advertise

"Relax. This is a discussion. Anything said here is just one engineer's opinion. Email in your dissenting letter and it'll be published, too."
This Web Site Is Modified Every 2-3 Days
Copyright 1991-2024 John Cooley.  All Rights Reserved.
| Contact John Cooley | Webmaster | Legal | Feedback Form |

   !!!     "It's not a BUG,
  /o o\  /  it's a FEATURE!"
 (  >  )
  \ - / 
  _] [_     (jcooley 1991)