Abstract eyes paradigm shift in verification

Electronic News, Feb 16, 1998 by Ann Steffora

Fremont, Calif.--As designs move to deep-submicron geometries, and as chips become more complex and increase in size, current verification techniques will fall short of the verification task. Over the next few years, the formal verification tool market will likely get more attention as ASIC companies seek a solution to make sure their designs do what they are actually supposed to do.

One approach that seems to make a lot of sense would be to write the specification for the design correctly the first time, which may not always happen.

Abstract, Inc., the U.S. counterpart of U.K.-based Abstract Hardware Ltd., has a solution. "In order to eliminate headaches further down in the design flow, Abstract is planning to leverage its theorem-proving technology it calls Lambda to come up with a methodology that is 'correct by construction.' This is done by creating the specification for the system design at a much higher level of abstraction--higher than the RTL or behavioral level--at the system level, by using a system-level design language," explains Farshid Tabrizi, director of sales support for Abstract. However, Mr. Tabrizi cautions that theorem-proving technology is still years out and requires a paradigm shift in the way designers currently work.

Further, with regard to mainstream use, Abstract says it can always find customers that have a need as well as expertise and patience to use it, but Lambda is not pushbutton. The technology has been sold and utilized by a number of European companies, including GEC Plessey Semiconductors; however, at the current state of the tool, one must be have a Ph.D. in mathematics to understand how to use the tool, explains Mek Rahmani, president and CEO of Abstract. Work will be done to make the tool easier to use, but that may take a few years.

In the near future, designers will have to deal with checking the interaction of 10 million gates, but how does one do that? "The answer is to build it correctly from the start. It is a sterilzed environment where the source is pure," Mr. Rahmani says. "Theorem proving takes customers all the way through from specification to design and teaches how not to make mistakes in the first place, which eliminates the need for testing," he explains.

With theorem proving, one writes in a formal system-level design language (SLDL), which extends Verilog and VHDL to describe the system at a higher level of abstraction. Anything later will be compared with the formal language. If a rule is violated, the tools tell you where. It is like on-line design rule checking--but on a grander scale, Mr. Rahmani says.

Model checking is a step toward this way of thinking, because it forces designers to think about properties versus vectors. Therefore, Abstract is currently concentrating on model checking, and will make this a focus for years to come. Model checking technology, which Lucent Technologies/Bell Labs Design Automation has seen success with, adds existing value to current methodologies. Formal techniques are not meant to replace simulation; just as static timing analysis complements simulation for timing, formal verification techniques do the same for functionality of a design.

CheckOff-M is Abstract's model checker which allows designers to find errors in a design and to verify critical properties, such as the absence of deadlocks and whether the design performs specified functions. A set of logical properties is provided which the design should possess, and the tool indicates if the design omits required behavior or includes unwanted behavior.

Abstract's tool also performs property-based design verification, where the user defines the characteristics the design should exhibit. These characteristics include safety, to make sure the design doesn't do something; and liveness, to make sure a behavior will happen eventually. A third characteristic, which the Lucent tool cannot verify, is a complex property, which indicates that something happens within a certain time period. However, it is understood that Lucent is also working on adding a complex property feature to its FormalCheck tool.

CheckOff-M can be used at all stages in the design flow because it can check behavioral, register-transfer level (RTL) and gate-level designs. CheckOff-M works with VHDL, EDIF and Verilog designs.

Recently, Abstract added a reduction algorithm called FASTEST to the CheckOff-M tool, in order to better compete with Lucent's tool, which offers a comparable capability.

Another key feature of the Abstract product is automatic generation of a diagnostic sequence and VHDL or Verilog testbench if two designs differ. The test bench generates test vectors to show the differences in the designs, then the tool automatically generates an initialization sequence for sequential circuits and finds a reset state.

CheckOff-M is integrated closely with CheckOff-S and CheckOff-E, Abstract's equivalence checking formal verification tools. CheckOff-S, like Chrysalis Symbolic Design's DesignVERIFYer, compares two state equivalent designs to determine if they are structurally equivalent. Two netlists with the same number of registers are compared with the other. As well, for every implied flip-flop at the RTL level, there must be a flip-flop at the gate level. According to Abstract, where Chrysalis falls short is allowing the tool to run at the full chip and system level, and it allegedly has problems on designs larger than 150,000 gates. Abstract has been told that a design of this size of design requires one gigabyte of RAM on the Chrysalis tool. Abstract claims that an ASIC foundry in Japan is running a 1.5 million-gate design on the CheckOff-S tool.