Posts Tagged ‘Jasper’

Remaking The Design Landscape

Thursday, January 28th, 2010

By Ed Sperling

Every now and then a new trend comes along in the semiconductor design world, often because an old tool doesn’t work well anymore or because a new one is achieving critical mass. Lithography moved to immersion when the wavelength couldn’t be refracted far enough anymore. Designers at the advanced end of Moore’s Law began using tools like high-level synthesis and Transaction-Level Modeling 2.0 to help sort out the complexities of multicore, multi-voltage, multi-power island designs.

What’s changing at 32nm and beyond is the number of different directions the industry is heading. In the past, each new node brought new changes. At 130nm, the changes were considered extremely difficult because manufacturing moved from 200mm to 300mm wafers, added copper interconnects and low-k dielectrics for insulation. Most developers and chipmakers heaved a sigh of relief when that transition was over. But in retrospect, that was relatively tame.

Interviews with dozens of engineers, vendors, scientists, researchers and business managers over the past six months show that what’s ahead cannot be bounded into just one or two shifts. The change under way now is geographically global. It’s moving to a higher and higher level of abstraction, from semiconductor to system to device. And it is as much driven by business as technology. Moreover, taken in total these changes will completely alter the basic fabric of the design community in ways that have never been seen before.

Business
Behind many of the changes afoot in the market there is always a business case. In the past, technology trumped business. Those with steely nerve and enough backing could often carve out a space for themselves in markets, and even if they weren’t entirely successful they could minimize their losses.

Three things changed over the past decade to alter this approach. Business now trumps technology in almost all cases. First, the venture community has grown more cautious about the rate of return in hardware and EDA tools ever since the dot-com bubble burst in 2001. It’s not possible to return to the tap anymore without a real product and a real business model.

Second, the cost of failure has gone up. It now costs $4 billion to $5 billion to build a state-of-the-art fab. Consortiums of very large companies and governments are now involved in this business. And it can cost upwards of $100 million to build a very complex SoC at the latest process node. Stalwart adherents to Moore’s Law such as Freescale, which made the leap to the next process node without hesitation until 90nm, have begun skipping nodes on certain products.

Third, chips are now so complicated that it takes too long to build everything from scratch. That means chipmakers must buy IP from third parties. Even Intel doesn’t make everything itself anymore. And all but a very few companies now use a fabless or fab-lite model for at least the digital portion of their chips, which forces them to adhere to design rules and process technology developed by the foundries.

Put these together and the result is that business issues are forcing a handoff of some of the most basic parts of semiconductor engineering—defining a unique architecture, tinkering with the layout, refining the process, and balancing all of these pieces together at tape-out. Fast yield, time to market and standardized interconnects and IP are no longer just goals. They are requirements. Some companies have handed off the building of chips entirely to a new class of value-chain producers like eSilicon, Global Unichip and Open-Silicon.

Globalization
For the first 50 years of its existence, the semiconductor industry defined global as North America, Europe and Japan. Taiwan was a latecomer to the part, and TSMC’s vision of a foundry model was considered revolutionary well into the 1990s. Companies like Texas Instruments and AMD said they had no intention of letting go of their own fabs.

Fast forward through two downturns and 10 process nodes and the situation now looks much different. Software is increasingly a part of the design process, heavily automated foundries can be located anywhere in the world where tax breaks and the cost of power are lowest, and massive education programs are under way in multiple countries that see semiconductor and computer engineering as a fast way to economic health.

While many lament that the semiconductor industry is declining or not showing growth, the opposite is happening. It’s expanding significantly. In 1977, the Semiconductor Industry Association reported total semiconductor sales of $2.88 billion, with about $1.92 billion of that in the Americas and only $182 million in Asia/Pacific (not including Japan). In the first 11 months of 2009, sales were $196 billion worldwide, with $102 billion in Asia/Pacific and $33 billion in the Americas.

By any standard this represents an enormous increase in sales, but the profits are now far more dispersed around the globe. Moreover, IP for chips is being developed in places like Eastern Europe and former Soviet republics, and in the future that kind of work will accelerate in other parts of the world because the barrier to entry into this market is one of the lowest—you don’t need to build full systems—while the return on investment is one of the highest. Virage Logic, ARM and Synopsys have been snapping up these kinds of operations around the globe over the past couple years.

Technology
Most of these changes are being driven by the technology itself. There are fewer design starts for ASICs these days, but the problems being solved are far more numerous on each chip than in the past. The tradeoffs of area, power and performance have been relatively balanced over decades of development. When lithography became an issue, there was enough slack in power and performance to tide chip designers over until the next node.

At 90nm that began to change. Classical scaling ended, lithography stalled at 193nm, defect density increased as irregularities in silicon and process technology became evident. Power forced even companies like Intel to begin adding more cores onto a chip rather than continuing to turn up the clock speed, creating problems about what to do with more and more cores.

At 22/20 nm—the next node for companies that live on the edge of Moore’s Law—things get even more interesting. Both Synopsys and Mentor Graphics predict that FinFETS will start showing up on chips—3D transistor structures that will wreak havoc on parasitic extraction because of the amount of data that will now need to be analyzed and synthesized. IBM has talked about potentially reducing the functionality on chips at future nodes to be able to get chips out the door that fit into the power budget.

All major chip companies are now looking at heterogeneous cores instead of homogeneous cores and matching software and core size for a specific function. IBM and Mentor are experimenting with computational scaling to compensate for the limits of 193nm lithography. And power techniques that used to be considered exotic and extraneous are suddenly becoming necessary.

Even substrates are changing. Intel, which examined and then rejected partially depleted silicon on insulator (SOI) is looking seriously at fully depleted SOI for future nodes. And work is under way to sidestep much of this entirely with 3D stacking of chips, which have many problems such as heat dissipation and parasitic issues still not fully understood.

Abstraction
Perhaps even more daunting in this whole process is a complete shift in control within the design flow. The number of computations necessary at advanced nodes, coupled with business pressures and time to market issues are forcing engineers to rely on models. For many, this is like black-box technology. You put requirements in one side and the software adds a lot of the things in between.

For engineers who learned to solve problems the hard way–that is, without software models–this is perhaps the toughest change of all. RTL engineers who work at big chipmakers say there is enough work at the moment to stick with their core competencies. The problem is the amount of data they are dealing with is going up, and over the next few years it will skyrocket into the stratosphere.

Japan has been particularly accepting of tools like TLM 2.0, high-level synthesis from companies like Mentor, Forte Design Systems and Synopsys, and network-on-chip technology from companies like Arteris and Sonics. The acceptance level in Europe is lower, and it has been lower still in North America. But that is likely to change at future process nodes as business pressures take root, something that is already becoming evident with the rapid proliferation of DFM tools and automated test suites.

Tools vendors characterize these changes as a shift from design engineer to systems engineer. But there’s far more to it than that. In the future, a systems architect will have to understand how the software will behave in the system they’re designing and how all pieces of the verification can be matched to the progress in the design. The next phase of systems engineering will be concurrency in multiple pieces of the design, with real-time feedback across the flow to make a series of modifications and more modifications until tape-out.

This is already evident in the number of tools players around the fringes that are trying to solve unusual problems–companies like Atrenta, Jasper, Oasys, CoWare, and a slew of others that have made inroads and will continue to make inroads.

Conclusion
Taken as a whole, the confluence of a variety of factors ranging from technology to tools to business is coming to a head. Each node from here gets tougher not because one problem has to be solved, but because more and more problems have to be solved simultaneously at each successive node.

Moore’s Law will continue, but not in the form in which it was originally conceived. A FinFET is not a classic transistor, and 3D stacking moves things into a different plane. Moreover, the tools to create these new devices will continue to change, the way they are manufactured will change, and the skills necessary to create these structures will change.

Perhaps even more important, all of these changes will begin showing up over the next couple of process nodes. We are all living and working in interesting times, but whether it’s a blessing or a curse may depend on each engineer’s role, their training, their ability to accept change and possibly even where they’re located

Formal Verification 101

Wednesday, May 27th, 2009

By Clive “Max” Maxfield

The first time I came into contact with the concepts of a digital hardware description language (HDL) and digital logic simulation, I inherently understood how it all “worked.” The idea that the statements in the modeling language acted in a concurrent manner just seemed to make sense.

By comparison, trying to wrap my brain around formal verification has always made my head hurt. I remember one year at DAC making a point to visit all of the EDA vendors with a formal verification presence and ask them to explain things like the difference between an “attribute” and a “property”.

They were all kind enough to do so. The only problem was that they all said completely different things and defined terms in completely different ways. Personally, I prefer a simple story that doesn’t make my eyes water, so here’s my “101″ version of the Formal Verification Space (where no one can hear you scream.)

Different Formal Flavors

As a tidbit of trivia, formal verification isn’t as new as many people believe. Although many of us weren’t aware of it at the time, large computer and chip companies like IBM, Intel, and Motorola actually started developing and using formal verification tools internally since the mid-1980s.

For quite some time, a lot of folks considered the term “formal verification” as being synonymous with “equivalency checking,” where an equivalency checker is a tool that uses formal (rigorous mathematical) techniques to compare two different representations of a design – say an RTL description with a gate-level netlist – to determine whether or not they have the same input-to-output functionality.

In fact, equivalency checking may be considered to form a sub-class of formal verification called “model checking,” which refers to techniques used to explore the state-space of a system to test whether or not certain attributes are true. Those attributes are specified in the form of assertions/properties. (Definitions of terms such as “property” and “assertion” are presented later in this article.)

Another category of formal verification known as “automated reasoning” uses logic to prove – much like a formal mathematical proof – that an implementation meets an associated specification. But that’s outside the scope of these discussions. For the purposes of this article, we shall focus on different aspects of the model-checking domain.

Why is Formal Cool?

It can be difficult to wrap one’s brain around formal verification, so let’s take this step-by-step. Suppose we have a digital chip design that consists of a number of functional blocks. Let’s further assume that we have an RTL description of each block. Before we connect them all together, how are we going to verify each block to ensure that it performs the task we require of it?

One way would be to create a testbench comprising a sequence of signals we wish to apply to the block’s inputs, along with the responses we expect to appear on the block’s outputs. We would then use a digital logic simulator to apply our stimulus to the virtual (RTL) representation of our block to see if it functions as planned.

Although useful, this approach has several issues we need to consider. In the case of the testbench (which we have to create), this will only verify the cases we thought to test. What about those slippery little “corner cases” we didn’t even think about? (In this context, a general definition of a “corner case” or “corner condition” would be a hard-to-exercise or hard-to-reach functional condition associated with the design.) Even worse, when we gather multiple blocks together, we have to discard our original block-level testbenches and create a new one from the ground up.

As an alternative, we could associate one or more assertions/properties with our block. These assertions/properties may be associated with signals at the interface to the block and/or with signals and registers internal to the block.

A very simple assertion/property might be along the lines of, “Signals A and B should never be active (low) at the same time.” But these statements also can extend to extremely complex transaction-level constructs, such as “When a PCI write command is received, then a memory write command of type xxxx must be issued within 5 to 36 clock cycles.” And yet another form of assertion relates to the assumption a designer makes when implementing a block, such as “I assume that I will never receive three writes in a row.”

One really important concept here is that of verification reuse. Once you’ve associated a bunch of assertions/properties with a block, they remain valid when that block is combined with other blocks to form a cluster of blocks or an entire system. For example, those assertions/properties that relate to implementation assumptions will ensure that these assumptions remain true or they will issue appropriate error messages.

Static vs. Dynamic

For the purpose of these discussions let’s stick with a simple assertion/property such as, “Signals A and B should never be active (low) at the same time.” One term you will hear a lot of is assertion-based verification (ABV). This comes in two flavors: static formal verification and dynamic formal verification.

In the case of static formal verification, an appropriate tool reads in the functional description of the design (typically at the RTL level of abstraction) and then exhaustively analyzes the logic to ensure that this particular condition can never occur (or that it defiantly will occur depending on what you are trying to do).

By comparison, in the case of dynamic formal verification, an appropriately augmented logic simulator (or post-simulation analyzer and debugger) will flag a warning if this particular condition ever does occur (or if it doesn’t occur – again, this depends on what you are trying to do).

One problem with static formal verification is that it can typically be used for only small portions of the design, because the state space increases exponentially with complex properties and one can quickly run into a “state space explosion.” By comparison, logic simulators can cover a lot of ground, but they do require stimuli and they don’t cover every possible case.

In order to address these issues, some solutions combine both techniques. For example, they may use simulation to reach a corner condition and then automatically pause the simulator and invoke a static formal verification engine to exhaustively evaluate that corner condition. Once the corner condition has been evaluated, control will automatically be returned to the simulator, which will then proceed on its merry way.

As a simple example of where this might be applicable, consider a first-in first-out (FIFO) memory. Its “Full” and “Empty” states may be regarded as corner cases. Reaching the “Full” state will require a lot of clock cycles, which is best-achieved using simulation. But exhaustively evaluating attributes/properties associated with this corner case – such as the fact that it should not be possible to write any more data while the FIFO is full – is best achieved using static techniques.

Assertions vs. Properties

It should be noted that the following was gleaned from my talking with lots of folks and then desperately trying to rationalize the discrepancies between the tales they told.

The term “property” comes from the model-checking domain and refers to a specific functional behavior of the design that you want to formally verify. For example, “after a request, we expect a grant within 10 clock cycles.”

By comparison the term “assertion” stems from the simulation domain and refers to a specific functional behavior of the design that you want to monitor during simulation, and therefore flag violations if that assertion “fires.”

Today, with the use of formal tools and simulation tools in unified environments and methodologies, the terms “property” and “assertion” tend to be used interchangeably – that is, a property is an assertion and vice versa.

In general, we understand an assertion/property to be a statement about a specific attribute associated with the design that is expected to be true. Thus, assertions/properties can be used as checkers/monitors, or as targets of formal proofs, and they are usually used to identify/trap undesirable behavior.

Formal Languages and Stuff

This is where things could start to get really confusing if we’re not careful. We’ll start with something called Vera, which began life with work done at Sun Microsystems in early 1990s. It was provided to Systems Science Corp. somewhere around the mid-1990s, which was in turn acquired by Synopsys in 1998.

Vera became an entire verification environment that encapsulates testbench features and assertion-based capabilities, and Synopsys originally promoted it as a standalone product, with integration into the Synopsys logic simulator. Sometime later, due to popular demand, Synopsys opened things up for third-party use by making OpenVera and OpenVera Assertions (OVA) available.

Somewhere around this time, SystemVerilog was equipped with its first-pass at an “assert” statement. Meanwhile, due to the increasing interest in formal verification technology, an Accellera standards committee started to look around for a formal verification language it could adopt as an industry standard. A number of languages were evaluated, including OVA, but in 2002 the committee eventually opted for the Sugar language from IBM.

Just to add to the fun, Synopsys then decided to donate OVA to the Accellera committee in charge of SystemVerilog (this was a different committee than the one evaluating formal property languages). Now pay attention because this bit’s confusing. Although Synopsys had donated OVA to Accellera, the folks at Synopsys also kept using OVA themselves. Meanwhile, like most standards committees, Accellera can’t accept a donation like OVA “as-is” because that would give the donating vendor a competitive advantage. Thus, they modified the OVA syntax and changed some of the underlying fundamentals to come up with SystemVerilog Assertions (SVA).

Yet another Accellera committee ended up in charge of something called the Open Verification Library (OVL), which refers to a library of assertion/property models available in both VHDL and Verilog 2K1.

So now we have the assert statements in VHDL and SystemVerilog, OVL (the library of models), OVA (the Synopsys-specific assertion language), SVA (the SystemVerilog version of OVA), and the Property Specification Language (PSL), which is the Accellera version of IBM’s Sugar language. It’s also probably worth noting that the latest versions of SVA and PSL are syntactically consistent in many respects.

Are we having fun yet?

The advantage of PSL is that it has a life of its own in that it can be used independently from the languages used to represent the functionality of the design itself. The disadvantage is that it doesn’t look like anything the hardware description languages design engineers are familiar with, such as VHDL, Verilog, C/C++, etc., but then neither do OVA or SVA. There is some talk of spawning various flavors of PSL, such as a VHDL PSL, a Verilog PSL, a SystemC PSL, and so forth. The syntax would differ between these flavors so as to match the target language, but their semantics would be identical.

As usual, it’s difficult to wrap one’s brain around all of this, but perhaps Figure 1 will provide a useful visualization.

Figure 1. Trying to put everything into context and perspective.

Figure 1. Trying to put everything into context and perspective.

It’s important to note that this illustration just reflects one view of the world and not everyone will agree with it. I flatter myself that some folks will consider this to be a brilliant summation of an incredibly confusing situation. On the other hand, others will doubtless regard it as being a gross simplification.

Who Are All the Players?

This is where things really start to get fun, because I’m sure to leave someone out and then they will get cross with me and I’ll be struck off their Christmas card list.

Of course, it practically goes without saying that the “big boys” in this arena are Synopsys, Mentor Graphics and Cadence. Also, there used to be a positive plethora of independents, but many of these seem have either been acquired or to have fallen by the wayside. Of the independents that are still standing, the ones that spring to mind are Calypto, Jasper, Real Intent and OneSpin.