|
Formal Specification of Interface Protocols
Interfaces between components of a computer system, either internal to a chip or between chips, are vulnerable to design errors resulting from different interpretations of the specification documents by different chip designers. A formal specification of an interface protocol provides a more complete and less ambiguous description, thus preventing costly errors early in the design process. In addition to providing an accurate reference model, formal specification has important benefits during the design verification process. Simulation checkers, assertions for formal verification, coverage tasks and interface monitors are automatically derived, saving enormous manual effort and improving verification quality. The OneSpec project provides methodology and tools to facilitate the definition of formal specifications for interfaces and to automatically generate specification derivatives.
Verification of Soft-Errors Detection Logic
As chip technology progresses in terms of reduced transistor size and reduced voltage, chips become more vulnerable to radiation-induced transient errors (soft errors), mainly caused by cosmic rays and emission of alpha particles. In order to make chips more robust, designers add special logic to detect and correct soft errors. This process, in addition to being labor-intensive, has a significant cost in terms of area, power and timing. The aim of this project is twofold: 1) Find soft errors that are not covered by the detection logic. 2) Propose solutions that close the vulnerability gaps while minimizing redundancy and overhead. We use formal verification methods to perform the analysis statically and hence more comprehensively than simulation based fault injection.
| |
|
