Checking the Play in Plug-and-Play

The adage for the age of system-on-chip may well be a twist on the age-old Latin maxim caveat emptor. For "Buyer, beware!," read "Buyer, be aware!"

It's surprising to realize that buyers of intellectual property (IP) blocks used in system-on-chip (SOC) designs may not be entirely aware of what they're getting and how it works. But that's one reason why software for IC design verification is gaining attention: to ensure that those blocks will work as intended, both internally and with other components.

Another reason is time to market. SOC providers could shorten their time to market considerably if they didn't have to spend up to 70 percent of it verifying that their designs will plug and play. SOCs are complex designs that fit most or all of the circuitry required for a cellphone, for instance, or a Bluetooth radio on a single IC. As their numbers and complexity increase, the design verification gap is widening. But help is at hand in a new type of design verification called assertions-based verification, although a looming standards battle threatens to slow its widespread adoption.

The intellectual property challenge

Already, to speed up design, many SOCs are assembled from predesigned circuit blocks, referred to as virtual components or intellectual property blocks. These IP blocks describe digital signal processor and microprocessor cores, memory management units, interface circuits, and more. They may come from a company's own cache or they may be licensed from third-party IP providers.

The strong demand for IP blocks has fostered a robust US $700 million third-party IP market. But a major challenge for these IP providers and their customers is to ensure that all the IP blocks will work--and work together--when they are slipped into designs.

And there's the rub. Often so little is known about the inner workings of the IP blocks that it is next to impossible for SOC designers to devise verification schemes to make sure their circuits work as intended.

"When you buy a piece of IP, some interface block for example, you don't know the ins and outs of that particular piece of IP, so you end up spending most of your money on [customer support services] and not on the IP per se," says Ron Chaffee, senior vice president of engineering for Conexant Systems (Newport Beach, Calif.), which buys IP for use in the chips it makes for both networking and mobile communications applications.

Chaffee explains that the frustrations of SOC integrators in dealing with third-party IP arise from a lack of "inventor's knowledge," a direct result of their dependence on IP delivered as a black box. That lack of knowledge reverberates, and aggravates, all down the line from SOC designer to end customer. "When your customers end up having trouble [with your SOC], there's nothing quite as irritating to them as hearing that you're not real sure what the answer is and you'll have to find out from your IP provider," Chaffee laments.

Assertions-based verification may be the light at the end of the black box tunnel. Assertions are chunks of code that describe how a design's logic is intended to behave. They are embedded into the hardware description language (Verilog or VHDL) code that describes the IP block's logic at the register transfer level (RTL). When this RTL code is fed into a design verification program, the program can check assertions to determine whether the block behaves as it should.

Assertions can be created in a few ways. Most assertions-based verification tools automatically create rudimentary assertions by extracting certain properties that describe simple behaviors directly from the RTL code. These assertions are used to check, for instance, that two signals never contend for a certain bus at the same time.

Assertions are also derived from specifications written by the block designer. The problem with doing it this way is that it requires more work from already overworked design engineers.

While it has been possible to employ assertions using VHDL code since the 1980s, the technique didn't begin to spread at all widely until the mid-1990s. Then Hewlett-Packard verification engineers Harry Foster and Lionel Bening (and others, too) asked themselves how they could ease the process of making a design's intent explicit. Foster and Bening were trying to get H-P's design engineers to specify exactly how their portion of a chip design was expected to perform. To relieve their design colleagues of the burden of writing complete specifications, Foster and Bening produced prepackaged modules of code to embed into the RTL, stating how basic elements of the design's logic were supposed to function. When the H-P engineers ran their RTL code in their verification tools, the tools processed the assertions to check whether or not these elements would behave as intended.

A modest number of assertions

Foster's work at H-P led to the Open Verification Library (OVL), which now belongs to Accellera, the standards organization of the electronic design automation industry. Last year Verplex Systems Inc. (Milpitas, Calif.) donated the library to this organization. Incidentally, the donor is a provider of verification software, where Foster is now chief architect. The OVL can be downloaded and used for free with both Verilog and VHDL verification tools. Most of the library's 35 or so generic assertions refer to conditions a designer would repeat often throughout a design, such as asserting that a particular event should never happen (assert_never), or it should always happen (assert_always), or it should always follow another specific event (assert_next).

When a verification tool reads the assertion module that the designer has embedded in the RTL, the tool calls in to the OVL, which contains all the logic needed to check that assertion. This library element may be tens or hundreds of lines of code long, says Dino Caporossi, vice president of marketing for Verplex Systems. For instance, assert_handshake, which means that a handshake protocol should be executed between two blocks when they communicate, has 200 lines of code.

"In the past, when Verilog or VHDL designers wanted to [test for] these conditions, they would have to manually enter this code," Caporossi said. "We provide them with templates so they don't have to do all this manual work."

The rest of the electronic design automation industry has now recognized the utility of these assertions. In the last three years, companies such as 0-In Design Automation, @HDL, Real Intent, Averant, and, of course, Verplex Systems have introduced verification software tools that rely on assertions. These assertions-based solutions to design verification are an extremely reliable way to ensure that a block's logic functions as the designer intended. They are of great help to third-party IP vendors, such as ARM and Tensilica (on which more later), and to SOC designers trying to integrate outside IP or reuse blocks generated internally.

Quite a few verification tools can take advantage of assertions. Simulators traditionally apply sequences of test vectors to the inputs of a given block of code to stimulate the RTL model, and then observe the output. Similarly, a simulation program such as Cadence's NC-Verilog or NC-VHDL, Synopsys' VCS, or Mentor Graphics' ModelSim can check an assertion written into Verilog or VHDL code to see whether it holds true. Simulators can also digest assertions generated by proprietary verification suites such as Real Intent's Verix, whose SimLink program automatically synthesizes Verilog checkers that a simulator can use to monitor user-defined assertions.

Once an assertion has been created to describe common conditions or events, that assertion can be used to check the entire design for any instance where that condition exists. Consider a designer who wants to make sure that the several FIFO (first-in, first-out) memories in a circuit block will not overflow. (This undesirable condition arises when there is an attempt to write data into an already full FIFO.) So he or she inserts a statement like assert_no_overflow into the RTL code wherever there is a FIFO.

When the FIFOs are tested in a simulation program, this tool calls the library to fetch out the logic associated with the assert_no_overflow library element. Next, armed with a fully functioning element, the tool checks whether the assertion holds true or if it has been violated for any FIFOs the designer wants monitored. Any overflow condition found is flagged by the tool, and the designer is alerted to the existence of a design problem close to where the assertion is violated. He must then debug the design to ensure that the overflow condition doesn't happen again. [See "How a Library Works"]

Verification engineers at Cisco Systems Inc. (Research Triangle Park, N.C.), under team leader Sean Smith, thoroughly exploited assertions on his team's most recent multimillion-gate SOC. They embedded 10 assertions into a single generic FIFO, which was reused on the chip 800 times, enabling his team to quickly and easily embed 8000 assertions for later checking in simulation.

Dual use

Versatility, as well as reusability, is a hallmark of assertions. In simulation, once inserted into RTL code, assertions can be used as monitors to detect incorrect behavior. And these same assertions can also be used in one important kind of formal verification approach. Called model checking, it proves mathematically that the logic depicted in the RTL model functions according to the properties and constraints--the assertions--specified in the design.

Model checkers see assertions either as properties inside a discrete block of code or as constraints that describe legal inputs to the IP block. A checker proves a property to be true given the rules specified by the constraints. When a formal tool reports that a property has been proven true, the designer can be 100 percent certain that the result is accurate--an ironclad guarantee no other verification method can offer. And the formal tool is very thorough, using complex algorithms to scour all possible states for examples where a property could fail. So exhaustive is the model checker that it will find bugs the designer would never think to test for [see flow diagram].

Interblock protocols

Because designers of IP blocks cannot anticipate every application or SOC where their design will be embedded, the rules--protocols--associated with signals passing through an IP block's interface from other parts of the chip must be thoroughly verified. Designers of third-party IP can make life easier for their customers by inserting assertions that act as protocol monitors at the block's interface, suggests Thomas L. Anderson, vice president of applications engineering for 0-In Design Automation (San Jose, Calif.).

For instance, a designer can embed an assertion that states that a set of inputs to the interface must always be one-hot. One-hot means that only 1 bit of a given incoming set of bits may be active at any given moment. When the IP block is added to an SOC and tested in a simulation program, the program will check to see whether the assertion holds true--that the set of inputs are indeed always one-hot. But if the tool finds an instance where the inputs coming into the interface are anything but one-hot--perhaps 2 bits are active simultaneously--the violated assertion will be flagged. The designer will be alerted and can then debug his design knowing what has gone wrong and where. Information as complete as this is difficult to come by using plain vanilla simulation.

"If we have a bunch of assertions on the interface that define how that interface is supposed to operate and if we define assertions that check to see if that behavior is being followed, then there's substantial benefit for both the IP provider and the IP consumer," explains Cisco Systems' Smith.

While Smith is partial to open-source OVL, designers can also use proprietary assertion libraries. Instead of embedding assertion modules written in Verilog or VHDL, as with OVL, it is also possible to insert assertions as comments into the RTL code, but this time only a proprietary verification tool can understand them. These comments are known as pragmas.

For example, 0-In Design Automation allows designers to insert assertions as comments in Verilog RTL code, but in a syntax that only its formal tool 0-In Search can recognize. These pragmas reference elements in 0-In's CheckerWare Library, which may be rules for checking datapath structure, state machines, and arbiters, as well as interface handshaking rules. 0-In also provides a wide array of protocol monitors for standard buses. These come in handy when verifying how IP will interact with other blocks in an SOC design. Third-party IP vendor Tensilica Inc. (Santa Clara, Calif.) has recognized the advantages of this for its customers and ships an RTL version of its Xtensa microprocessor core embedded with 0-In's assertions. Those Tensilica customers who also buy the 0-In tool may run their own formal analysis and simulation using the embedded assertions.

Guaranteed IP

While Tensilica embeds 0-In assertions, it's the exception that proves the rule. ARM Ltd. (Cambridge, UK) is the world's most successful IP vendor in terms of annual revenues. Before committing one way or another to embedding assertions in its cores, ARM is waiting to see what standards take hold in the industry. Meanwhile, the company is simply shipping so-called verification IP (the AMBA Compliance Testbench) with its ARM microprocessor cores.

Internally, ARM uses formal verification to improve the quality of its RTL IP before it goes out the door. For this purpose, the company is currently using a tool for checking formal properties, Solidify, from Averant (Santa Clara, Calif.), which is built on that company's proprietary hardware property language, HPL.

ARM's Mike Turpin, a principal validation engineer, points out that while assertions and formal languages are both useful for verification, they have different strengths. Formal languages have a rich syntax and precise semantics that allow much more flexibility than a predefined or automatically extracted set of assertions. On the other hand, Turpin says, OVL assertions are "tool independent--they are just functions written in RTL--and can be used in different verification methodologies, including simulation, emulation, and semiformal and formal checking." So ARM is considering embedded assertions, particularly the OVL, as a potential verification methodology for both internal use and external distribution.

Formal property checking is a relatively new technique generally, and within ARM, Turpin and principal validation engineer Alan Hunter have been using the method for only about a year or so. But Hunter has already come to value the ability to completely verify the interfaces to internal blocks in a design. And, as Turpin says, besides finding faults no other method could detect, a property checker that passes a design gives you a 100 percent guarantee that the design has particular properties. Again, this is something no other tool can do.

False negatives

There are drawbacks, however. Averant's Solidify could indicate that a property is failing when in fact the formal analysis started from an unreachable state. The indication of such a failure is termed a false negative.

"False negatives can take a lot of time debugging and I think that's the hardest thing with these formal tools at the moment," says Turpin.

False negatives most often happen because the user has omitted something--a constraint to tell the tool the legal operating conditions, according to Ramin Hojati, president and founder of Averant. Over the last year, the company has introduced design constraints that allow the user to manually identify, and eliminate, states that would cause a false negative. Averant has also introduced an automatic constraint generator that the company says will eliminate most false negatives.

There's a good reason that ARM's Turpin and Hunter are willing to put up with the hassles of debugging the occasional false negative. They want to prove the quality of the code before it gets shipped and believe that exhaustive formal verification is the best way to do that.

"The formal tool will be a bit paranoid and test things that you'd never test"

"Every single customer will put our IP into a slightly different scenario, so the formal methods give you the advantage of checking every corner case [extremely rare condition], not just as many corner cases as we can think of or randomly generate," Turpin says. "The formal tool will be a bit paranoid and test things that you'd never test."

The battle over standards

For the greatest power and flexibility, verification engineers can write their own assertions, using a variety of multipurpose verification and formal property languages. Indeed, there are so many different languages of these two types that, combined with all of the open and proprietary assertion libraries, this burgeoning Tower of Babel is viewed by most people in the electronic design automation industry as the main barrier to wide adoption of assertions-based verification methods. For example, the languages Superlog from Co-Design Automation Inc. (Los Altos, Calif.) and e from Verisity Design Inc. (Mountain View, Calif.) both support an extensive range of property specifications. There are also a number of proprietary formal property languages, such as Averant's HPL.

Unfortunately, the babble might just be beginning as a battle heats up over which formal property language will be the standard. Just this past spring, Accellera chose to propose IBM's Sugar to the IEEE as the standard formal property language. Electronic design automation behemoth Synopsys Inc. (Mountain View, Calif.) is offering up the OpenVera 2.0 hardware verification language as the de facto industry standard. OpenVera 2.0 now incorporates Intel's ForSpec property language, which was snapped up by Synopsys after Accellera rejected it as a standard earlier this year.

Most vendors of formal verification tools say that they could convert their programs to comply with a standard property language. In fact, many would prefer to compete on the merits of their tools rather than the merits of a proprietary language.

Rajeev Ranjan, director of R&D for Real Intent (Santa Clara, Calif.), fervently believes that a common language will spur adoption of assertions-based verification, but that the Tower of Babel will rule until the industry settles upon a standard.

"[The industry] is just not going to be able to do all this SOC design, plugging all this stuff together, unless they use assertions," Ranjan says. "And IP vendors aren't going to adopt proprietary languages. They may use it to verify their IP, but I don't think the industry is going to start [embedding assertions] until there is standardization."

The burning question now is which formal property language will be accepted by the electronic design automation industry as the standard: Accellera/IBM's Sugar or Synopsys' OpenVera 2.0? There's also the distinct possibility that both formal property languages will be widely adopted, resulting in the same kind of needless duplication that has plagued the industry since Verilog and VHDL came on the scene in the 1980s.

"I do believe that the best language will ultimately win in the marketplace--probably by the other languages mutating or incorporating its best features," says Carl Pixley, a senior director in Synopsys' Advanced Technology Group.

While Synopsys pushes hard for OpenVera 2.0 and many of the smaller assertions-based verification vendors are getting behind Sugar, two of the biggest companies in this industry might hold the key to which standard ultimately prevails: Cadence Design Systems Inc. (San Jose, Calif.) and Mentor Graphics Corp. (Wilsonville, Ore.). Buy-in from these two companies is the key to a formal property language's taking hold. And both are buying into Sugar. How hard these companies push Sugar could determine whether young purveyors of assertions-based functional verification are bought up or crushed, or whether they will have time to carve their own niche.

"We think it's going to facilitate the exchange of [IP] if we can get the rest of the EDA industry and the suppliers of IP to embrace this notion of a single standard for documenting IP using a property-based language," says Mike O'Reilly, vice president of marketing for Cadence's Systems and Functional Verification group. He also emphasizes that it's less important which language ultimately prevails as the standard than that the language works equally well with Verilog, VHDL, and formal methods. "Whether it's a Cadence-, Synopsys-, or a Mentor-driven system, that's not important. The bottom line is we need to ease the customer pain of being able to incorporate and digest IP."