EDA is dead (EE-Times) ?

Here is an interesting article from EE Times :)
--------------------------------------------------------------------------------
EDA is dead. Yes, it's still needed: We're not going to go back to designing chips with rubilith again. But the reality is that fewer and fewer chips are being designed, and most of the differentiation of a system is moving into the software. Even Gary Smith, the longtime Gartner analyst for EDA, proclaimed at the 2006 DAC that "It's the software, stupid." And then Gartner laid off Gary's EDA group, another symptom.


read the full article in ee times by Paul McLellan at

http://www.eetimes.com/news/design/showArticle.jhtml;jsessionid=5JLWEO0HWVLOOQSNDLOSKH0CJUNN2JVN?articleID=198001571

International work shop on Logic Synthesis

IWLS 2007, a premier work shop on logic synthesis and related technologies will be held at Paradise point resort & spa, San Diego, California from May 30th to June 1st 2007. Visit for more information.
www.iwls.org

1.1.2 Let's blame logic synthesis

why does an Equivalence Checker (EC) abort?
Because the left hand (EC) does not know what the right hand (logic synthesis) is doing. In a situation where Equivalence checking is not able to prove some of the compare points right or wrong, it has the tendency to create abort points.

How deep is the rabbit hole?

Equivalence checkers solve problems like BDD isomorphism and Boolean SATisfiability. They are inherently tough problems to crack. 20-30 years of research in this area (most active since 1986 ROBDD paper!) has made life less difficult. Data path verification and sequential checking are still major challenges which the industry faces today.

The equivalence checker goes through iterations of BDD isomorphism (comparing BDD's) -> SATisfiability checking -> ATPG -> Random Simulation to generate a proof of correctness or failure. In the event that one particular algorithm is not able to solve a problem instance, the problem instance seeps through to the other solver during the comparison process. Life gets only more complex in (Sequential Logic equivalence checking) SLEC.

lets us now assume that we have some problems which take extremely long run time or tremendous amounts of computer memory for computation. In the event of not being able to solve the problem within the given memory/run time requirement and after going through the sequence of solver iterations, the equivalence checker returns an abort to make "designer's life" miserable.

This still does not prove the compare point to be right or wrong :). In this situation the best thing to do is to move forward by generating functional vectors for simulating the cone of logic under consideration. (The formal tool did help you verify 90-95% or more of your logic :)), so dont worry, be happy!

If the cone of logic ends up being pre-verified IP (like Designware components and if confidence with these components is very high)these modules can be black boxed and formal verification can still be used on the remaining cones of logic.

As designers, we can do a couple of things to make life miserable for Formal verification engineers:

1. Sharing, Merging and Expression synthesis of (data path) operators.
2. Hierarchical vs flat comparison.
3. Dont care optimization.

What can synthesis guys do the alleviate the problem?
Sacrifice QOR :)

1.1.1. The Art of Equivalence Checking

Ever wonder why RTL to netlist verification is needed?
why is the process of Equivalence Checking (EC) so hard?

Read on.... :)

Logic Synthesis as a process is prone to Bugs. There are too many transformations happening in logic synthesis which can alter the netlist in a wrong manner and make it infer functionality other than what was intended in the original RTL. These bugs are not intentional but happen by accident during synthesis tool development. They can happen mostly during the elaboration stage as new verilog/VHDL constructs start showing up from time to time in new language standards. It takes time to build a robust Langauge analysis/elaboration engine as a front end to synthesis engine.

Now, How do we make sure we did not goof up our synthesis?

Simulation is not a robust proof of correctness as it was never intended to be exhaustive. However we can run the same functional vectors and check our netlist to see if we are lucky to catch a problem in gates. This is never a full proof verfication strategy.

Equivalence checking comes to the rescue. :). And it is fool proof. EC mathematically proves that the RTL and Netlist are equivalent and does not need functional vectors.

Most EC vendors give manuals along with the tools which explain how to configure these tools for various scenarios like

1. retiming
2. clock gating in Netlist
3. scan inserted netlist
4. Cut point insertion
5. Hierarchical verification/debug
6. Constant propagtion

to name a few. There might be more and the list is not comprehensive by any means. :)

The tools (Verplex/Fromality) also have a nice Debussy like interface to debug and pinpoint the cause of mismatch. These tools also write out failing vectors which can be used by a simulator for further debug.

EC does have it's set of difficulties when performing the following operations..

1. ACMP (Automatic compare point matching)
Before the proof starts, correspondence has to be established between the golden (RTL) and revised (Netlist) circuits. There are various techniques like name based matching, structural matching, prover based matching and ATPG to accomplish this.

2. verifying difficult SAT instances

3. Verifying data path components like Multipliers/dividers.

Operations are easier at word level (Binary Moment diagrams) than bit level for arithmetic circuits. However, the problem is in obtaining word level diagrams from bit level representation. Bit level operations on arithmetic circuits are very inefficient and memory/runtime intensive. ILP (Integer linear proramming) approaches are very popular but they fare poorly on control logic and work well on data path.

This is a very hot and active area of research in Formal community. :)

4. Difficulty in reaching counter examples as the generated counter example might not be reachable in normal circuit operation.

5. Equivalent cut point insertion

Formal tools internally find cut point equivalences to break a big problem into smaller sub problems to solve it more efficiently (using BDD + SAT). If cut point equivalnces are not correctly determined (most tools use ATPG for finding these equivalences), the formal tool may show false Negatives to the end user and create unnecessary panic!.

6. Identifying boundary nets for data path components (as they need to goto a different solver)

Most of these problems stem from the structural dis-similarities which exist between RTL and netlist as they come from 2 different (synthesis and Verification) engines.

1.1. Formal Verification

Verification is a Major bottleneck in design flow. It consumes upto 75% of the overall design cost and effort. This is why several (Formal) methods have been proposed in recent times as alternatives to classical simulation to speed up the process.

We can split up Formal techniques into different categories like

1. Equivalence checking (EC)
2. Property Checking
3. Symbolic simulation

The development/application of various tools using these techniques accelerates the process of verification and also points out numerous weaknesses and bugs of these techniques (especially on complex arithmetic ckts like Multipliers) on industrial scale designs to CAD developers :)

The state of the art formal tools make use of..

1. BDD (Binary Decision Diagrams)
2. SAT (Boolean SATisfiability)
3. ATPG (Automatic Test Pattern Generation)
4. Model Checking (MC), Bounded Model Checking (BMC, for large ckts)
5. Symbolic Simulation
6. Random Simulation
7. Term rewriting
8. Word level approaches like Binary Moment Diagrams (BMD's).

Most industrial quality formal tools make use of more than 3-4 (Multi-engine approaches!) of the above mentioned techniques which often work orthogonally (tough to combine!) to solve the verification problem at hand.

Formal techniques are not only popular these days for digital circuts but are gaining immense popularity in proving Linear/NonLinear analog systems as well.

I will discuss equivalence checking next..

1. VERIFICATION

Verification is a huge topic and a number of books exist on the subject. As a goal of this blog, treatment of the topic has to be limited to a few aspects only.

Wrong functionality which does not meet the end specification results in products which dont meet customer expectations. Hence verification of the design is needed to make sure that the end specification is met and corrective actions are taken on designs which dont meet them. If verification does not catch a bug in design, wrong designs get out in to the market.

Coverage metrics are defined by most verification engineers. Based on the level of representation, here are a few coverage metrics..

1. code based metrics (HDL code)
2. Circuit structure based metrics (Netlist)
3. State-space based metrics (State Transition Graphs)
4. Functionality based metrics (User defined Tasks)
5. Spec based metrics (Formal or executable spec)

There are many branches to verification of digital systems.

Below we list a couple of them

1. Simulation (for digital systems)
2. Advanced formal verification of Hardware [equivalence checking, Assertions, Model Checking]
3. Hardware Acceleration (FPGA/Emulation), or hardware/software co-design for simulation..

Simulation aims to verify a given design specification. This is achieved by building a computer model of the hardware being designed and executing the model to analyze it's behavior. For the model to be accurate, it has to include as much information in it as possible to be of any realistic value. At the same time, the model should not consume too much computer memory and operations on the model should not be run time intensive.

There are numerous levels of abstraction at which simulation can be performed..
1. Device level
2. circuit level
3. Timing and macro level
4. Logic or gate level
5. RTL level
6. Behavioral level

The specification (for the computer model) for a digital system is usually written at a behavioral level or RTL level (we will discuss more about gate level sim later!) :). In addition to the design requirements in the spec, more behavioral or RTL code is written in the form of a wrapper (test bench) around the original design to test and see if the design meets the design intent. The wrapper logic probes the design with functional vectors, collects the responses and verifies them against the expectated response.

A simulator has a kernel to process an input description and apply stimuli on it and represent the result to an end user on a waveform viewer. Internally it creates models for gates, delay, connectivity and numerous other variables.

There are various logic simulators available from numerous CAD vendors. (ModelSim, ncVerilog, VCS). Most of these simulators are a combination of event driven and cycle based mechanisms. They can also handle mixed language designs (VHDL+verilog) and adhere mostly to the Language specification which the IEEE standards committee comes out with. Some of these simulators are mixed mode simulator, i.e they can handle multiple levels of abstraction.

Verification technology has matured over the years. We have many more mechanisms in place apart from simulation.

I will try to list a few of them below and we will cover each one in the future

Detection: Simulation, Lint Tools, Semi-formal, Random generators, Formal verification
Debug and comprehension: waveforms, debug systems, Behavior based systems which use formal technology
Infrastructure: Intelligent testbenches, Hardware Verification Langauages, Assertions

A good reference for verification is "writing Test benches by Janick Bergeron".

6.1. DFT (Continued)

I wish to thank john (www.dftdigest.com) for his comments on my last post on DFT. BIST drives the scan chains in the design.

One major advantage of BIST is that the chip can test itself and hence we can reduce or avoid time on the tester all together. Testers are costly equipment and time on the tester is expensive. Tester memory/speed determine the cost of the tester and it can run into millions of dollars. So by providing some test access points for covering those faults which were tough to cover by BIST, more fault coverage can be achieved using an external tester, but with less tester time as BIST was used to get a big chunk of the coverage already!.

MBIST is widely used in the industry (almost most memories on chip have an MBIST/MBIST interface!) but logic BIST hasn't really captured the imagination of designers yet!. Logic Vision and Mentor Graphics sell tools which automatically generate vhdl/verilog wrapper logic for these modules given a specification.