CARLSBAD, Calif. — A radically new approach to design and verification will be shown at this month's Design Automation Conference by Derivation Systems Inc., a formal-verification startup. Its Derivational Reasoning System (DRS) is a "formal synthesis" tool that guides users from a high-level specification to implementation with pre-verified steps.

Unlike any other offering from formal-verification providers today, DRS offers a complete design flow with a "correct-by-construction" approach. Just follow the synthesis steps and there's no need to run any post-design verification, said Bhaskar Bose, Derivation Systems founder and chief executive officer.

DRS was developed under a NASA contract and has been applied to such projects as an interface unit for an avionics embedded processor, an avionics altitude-command module, a subtractive division circuit and a 32-bit general-purpose microprocessor.

Because the methodology is so new, it's not sold as an off-the-shelf product but as part of a package, including services. "We would require some handholding in the beginning, but once a customer pushes through a couple of designs, we think they'll be able to do it on their own," said Bose.

Though Derivation Systems was founded in 1993, DRS marks its first foray into the commercial EDA marketplace. All of DRS' employees boast graduate degrees, with experience in formal verification and hardware/software development. Bose was a NASA fellow from 1991 to 1993 and received his PhD in computer science from Indiana University in 1994. M. Esen Tuna, senior research scientist and lead developer of DRS, also holds a PhD in computer science from Indiana.

In concept, DRS is similar to formal "theorem-proving" tools, in which a mathematical specification is progressively refined and proved at each step. Such tools have never gained a large following, due primarily to the difficulty of creating the original specification. Bose believes Derivation has solved that problem by taking a new approach with DRS.

Instead of having an underlying theorem-prover, Bose said, "our steps are already proven to be correct. The system just executes it. It checks whether the preconditions have been satisfied, and if so, it just goes ahead and does it."

The original specification is created in a proprietary, Lisp-like language that does not require a great deal of mathematical expertise, Bose said. Proprietary languages have not been popular among EDA users, but he said Derivation's language is simple and relatively easy to learn. The initial specification is strictly algorithmic and has no implementation details.

While the system offers some automation, it's largely interactive in nature. For example, it has some automatic scheduling and resource-allocation algorithms. But, Bose acknowledged, "to do it well, you'll have to do it manually. The algorithms are more to show how it could be used in an automated way."

DRS can take a design all the way through optimization and mapping to a gate-level net-list, Bose said. It has no ASIC library support, but it can generate Xilinx XNF net-lists for prototyping.

Alternatively, users can generate VHDL files. Bose said this VHDL "theoretically should be synthesizable" with Synopsys synthesis tools. But the company has so far targeted the academically oriented Alliance HDL compilers.

DRS is aimed now at hardware design. But it potentially offers a framework for hardware/software codesign, Bose said. "It has some very good partitioning." Because DRS comes with services, it has no set price, but Bose said $90,000 is a typical starting point. DRS runs on SunOS, Solaris, Linux and Windows NT platforms.

	eeProductCenter Launches SpecSearch®, New Parametric Parts Search Engine In our continuing effort to enhance our site, eeProductCenter introduces SpecSearch® powered by GlobalSpec. Click here.
Free Subscription to EE Times First Name Last Name Company Name Title Email address   Click here for your Free Subscription to EETimes Europe