Invention Grant
US08656330B1 Apparatus with general numeric backtracking algorithm for solving satisfiability problems to verify functionality of circuits and software
失效
具有通用数字回溯算法的装置，用于解决满足性问题以验证电路和软件的功能
- Patent Title: Apparatus with general numeric backtracking algorithm for solving satisfiability problems to verify functionality of circuits and software
- Patent Title (中): 具有通用数字回溯算法的装置，用于解决满足性问题以验证电路和软件的功能
-
Application No.: US12970851Application Date: 2010-12-16
-
Publication No.: US08656330B1Publication Date: 2014-02-18
- Inventor: Andreas Kuehlmann , Kenneth L. McMillan , Shmuel Sagiv
- Applicant: Andreas Kuehlmann , Kenneth L. McMillan , Shmuel Sagiv
- Applicant Address: US CA San Jose
- Assignee: Cadence Design Systems, Inc.
- Current Assignee: Cadence Design Systems, Inc.
- Current Assignee Address: US CA San Jose
- Agency: Alford Law Group, Inc.
- Main IPC: G06F17/50
- IPC: G06F17/50
Abstract:
In one embodiment of the invention, a design verifier is disclosed including a model extractor and a bounded model checker having an arithmetic satisfiability solver. The arithmetic satisfiability solver searches for a solution in the form of a numeric assignment of numbers to variables that satisfies each and every one of the one or more numeric formulas. Conflict in the search, results in the deduction of one or more new numeric formulas that serve to guide the search toward a solution. If the search finds a numeric assignment that satisfies each and every one of the one or more numeric formulas, it indicates that a functional property of the system is violated.
Information query
