Skip to main content


Formal Verification

User Feedback

IBM Haifa Chip Design Center (A Large Community of PSL/Sugar Users)
Our chip design groups in Haifa and Tel Aviv are both extensive users of PSL/Sugar and the tools driven by it. Specifically, we are committed to the use of FoCs and RuleBase Parallel Edition in our current and future project. These tools are among the key ingredients of our success as our ASIC design center. They fit naturally in our ASIC design flow. I checked in the last few DAC conferences, and I saw no tools in the market that gave the designers such simple way to finding bugs.

And I view PSL/Sugar as a key factor - actually, an enabling technology - in getting those tools accepted and so strongly leveraged by our design and verification engineers. The important properties of PSL/Sugar that made it happen are its simplicity, shortness, robustness, richness and beyond all those - its being multi-purpose, with support for both Formal Verification and the more traditional Simulation methodology (via FoCs).

The success and impact we see with PSL/Sugar - and the FV tools based on it - are documented in the presentations we made in several conferences, cf. our presentation in the fringe user meeting held at DAC'03, earlier this year.

Eli Bokshtein, Verification Manager

Mellanox Technologies (Licensee of RuleBase and FoCs)
We know that specifications are the root of good design and verification. In Mellanox, we work hard on documenting our design specifications documented.

Well, one of the first observations I made when I started to work on formal verification, is that the mental process of translating a chip architecture document into a set of Sugar properties to be verified is extremely simple. I attribute it, first and foremost, to the natural way by which Sugar expresses properties of state machines that all hardware are.

Overall, we find Sugar very easy to use, and as a specification formalism it pretty much satisfies all our needs.

Of specific strength is the fact that Sugar is "a language for all seasons": In the same project, you can see different people using different layers of Sugar for different verification problems. For example, our experienced verification engineers use the full strengths of the language with preference to pure CTL and accent to intrinsic existential properties; many other verification engineers typically focus on "sequence-->sequence" properties; designers and dynamic verification engineers write safety properties with further translation to Verilog checkers. I especially like the fact that most properties go either to simulation and to formal verification. This integrability of Sugar is among the cornerstones of our chip verification methodology.

Sergey Nemanov, Senior Verification Engineer

Zoran Microelectronics (Licensee of RuleBase)
Since 1998, the Zoran verification team has used RuleBase with good results.

Two features stand out in IBM's formal verification toolset. The first - and probably the most important - is the specification language Sugar. The second is the strong verification engine under the hood. While the second is an important technology component, the former - Sugar - is really what makes formal verification work for us everyday.

Our experience has led us to gladly recognize that Sugar is very easy to learn and use. It is expressive, mature, robust, and simply can do the job. Sugar is rich yet concise - and allows you to specify complex properties in a very clear way.

As our primary interface to formal verification, Sugar enables us to easily embrace advanced formal verification techniques coming from IBM.

Avi Parash, Verification Manager,
Digital Camera Products