Method and apparatus for coverage analysis of srt look-up table
AssigneeInternational Business Machines Corporation
InventorsElena Guralnik, Haim Kermany
Life of this patent
Estimating the term…
Abstract
A computer-implemented method, computerized apparatus and computer program product. The method includes receiving at a computing device, a Sweeney-Robertson-Tocher (SRT) implementation, and a look-up table (LUT) used by the SRT implementation; obtaining an assertion for the SRT, the assertion associated with at least one entry from the LUT; verifying the assertion by executing a formal verification engine on the SRT implementation. Subject to the assertion failing, the method further provides a counter example for a computation that when performed by the SRT implementation accesses the at least one entry. Further, subject to the assertion holding, the method performs determining that the at least one entry is unreachable.
Claims20
A computer-implemented method comprising:
- receiving a Sweeney-Robertson-Tocher (SRT) implementation, and a look-up table (LUT) used by the SRT implementation;
- obtaining an assertion for the SRT, the assertion associated with at least one entry from the LUT;
- verifying the assertion by executing a formal verification engine on the SRT implementation;
- subject to the assertion failing, providing a counter example for a computation that when performed by the SRT implementation accesses the at least one entry;
- and
- subject to the assertion holding, determining that the at least one entry is unreachable.
A computerized apparatus having a processor, the processor being adapted to perform the steps of:
- receiving a Sweeney-Robertson-Tocher (SRT) implementation, and a look-up table (LUT) used by the SRT implementation;
- obtaining an assertion for the SRT, the assertion associated with at least one entry from the LUT;
- verifying the assertion by executing a formal verification engine on the SRT implementation;
- subject to the assertion failing, providing a counter example for a computation that when performed by the SRT implementation accesses the at least one entry;
- and
- subject to the assertion holding, determining that the at least one entry is unreachable.
A computer program product comprising a computer readable storage medium retaining program instructions, which program instructions when read by a processor, cause the processor to perform a method comprising:
- receiving a Sweeney-Robertson-Tocher (SRT) implementation, and a look-up table (LUT) used by the SRT implementation;
- obtaining an assertion for the SRT, the assertion associated with at least one entry from the LUT;
- verifying the assertion by executing a formal verification engine on the SRT implementation;
- subject to the assertion failing, providing a counter example for a computation that when performed by the SRT implementation accesses the at least one entry;
- and
- subject to the assertion holding, determining that the at least one entry is unreachable.
Dependencies are inferred from the claim text.