FoCs (short for Formal CheckerS, pronounced "fox") Property Checkers Generator is a productivity tool for automatic generation of simulation monitors from formal specifications. It greatly aids chip designers and verification engineers in the complex, costly task of verifying chip designs before submitting them to manufacturing. FoCs Property Checkers Generator is being used by internal IBM users, as well as by external customers. Users report a drastic improvement (up to 50%) in "testbench" development time. FoCs Property Checkers Generator has been made an official component of Blue Logic Methodology.

How does it work?

FoCs Property Checkers Generator takes properties written in the PSL/Sugar specification language and automatically translates them into Checkers, or monitors, which in turn are integrated into the chip simulation environment. These Checkers monitor the simulation results on a cycle-by-cycle basis for violation of the properties. Each Checker implements a state machine that enters and asserts an error state if the respective property fails to hold in a simulation run.

FoCs Property Checkers Generator can also be used for coverage analysis, that is, to create checkers that track the occurrences of events of interest during simulation. FoCs Property Checkers Generator can produce code in Verilog, C++, and VHDL, and it supports the conventions of popular simulators such as Model Technology's ModelSim.

Gil Shapir, leader of the FoCs Property Checkers Generator and RuleBase projects, has led projects at the IBM Research Lab in Haifa, Israel, since 1996. Among these other projects were the Hermitage Museum project (Web site and interactive kiosk) and WAP hosting.

Anat Dahan, the former FoCs project leader, has also worked in the area of CSP (Constraint Satisfaction Problems). Mrs. Dahan joined the IBM Research Lab in Haifa, Israel, in 2001.

Dmitry Pidan has developed and maintained FoCs Property Checkers Generator since 2000. He is in contact with customers and is involved in the design of new FoCs features.

Ilan Beer has held various research and development roles in the IBM Research Lab in Haifa, Israel, since 1989. He initiated and led the development of IBM's breakthrough formal verification tool, RuleBase. Currently, Mr. Beer works on bio-informatics activity at IBM in cooperation with the Technion, Israel's Institute of Technology.

Yaron Wolfsthal, Ph.D., has held various positions since 1989 at IBM Almaden Research Lab, IBM Palo Alto Scientific Center, and IBM Haifa Research Lab. Since 1995, Dr. Wolfsthal has managed IBM's formal verification activities in the Haifa lab.