Verification is the science involved with the development of methods to analyze and determine whether a given implementation of a system conforms with its specification. With the exponential growth in system complexity, verification has become a true bottleneck in the development of software and hardware systems. In fact, over 50% of the resources invested in developing systems are reportedly spent on verification.
In our research, we work on developing techniques, algorithms and tools that will sustain and expand IBM's positioning in all areas of verification, including
Formal Hardware Verification (algorithmic and deductive methods)
Simulation based Methods (e.g. test generation and coverage analysis)
Software Verification
In our work, we will pursue the publication of papers in verification conferences, establish relationships with universities and professors, and in general take a key role in the verification research community.
Projects
- FoCs
takes Sugar properties (a.k.a. assertions) and translates them into HDL Checkers, which in turn are integrated into the simulation environment
- FPgen
Floating Point Test Generator
- Genesys
An Intelligent Test-Program Generator for Processor Verification
- Machine Learning
algorithms for automatic pattern recognition, prediction, analysis, classification, and learning of structures
- Meteor
a generic functional coverage tool
- Octopus
an umbrella for generic constraint satisfaction problem (CSP) activities
- PSL/Sugar
the specification language used by engineers to specify the functional properties of logic designs.
- RuleBase
industrial-strength formal verification (FV) tool, especially applicable for verifying the control logic of large hardware designs.
- X-Gen
model based random test program generator, oriented at the system level