Method for implementing formal verification of optimized multiplier via SCA-SAT synergy
US12292946B1 · kind B1 · utility
Assignee
Inventors
Key dates
| Filing date | Dec 4, 2024 |
| Grant date | May 6, 2025 |
| Priority date | — |
| Expiry date | Dec 4, 2044 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F17/16
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method for implementing formal verification of an optimized multiplier via symbolic computer algebra (SCA)-satisfiability (SAT) synergy includes: systematically recovering, by a reverse engineering algorithm, an adder tree from an optimized multiplier; 2) generating, by a constraint satisfaction algorithm, a reference multiplier only by using an adder based on a constraint condition; and 3) combining, by an SCA-based and SAT-based verification method, complementary advantages of SCA and SAT. In the verification framework, the method introduces a reference multiplier generator for generating a correct reference multiplier. The correct reference multiplier has both a structure similar to a structure of the optimized multiplier and a clear adder boundary. The clear adder boundary allows proving correctness of the correct reference multiplier through SCA-based verification. With a structural similarity between the reference multiplier and the optimized multiplier, the reference multiplier is used as a known correct model for SAT-based verification of the optimized multiplier.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.