| CPC G06F 17/16 (2013.01) | 4 Claims |
|
1. A method for implementing formal verification of an optimized multiplier via symbolic computer algebra (SCA)-satisfiability (SAT) synergy, comprising the following steps:
step 1: systematically recovering, by a reverse engineering algorithm, an adder tree from an optimized multiplier to ensure a structural similarity, wherein the reverse engineering algorithm comprises atomic block detection and an adder tree recovery algorithm;
wherein the atomic block detection is used to detect constituent atomic blocks of an And-Inverter Graph (AIG) of the optimized multiplier, comprising a half adder (HA), a full adder (FA), an XOR gate, and an AND gate, systematically extract all cuts from the AIG through AIGcut enumeration based on a constructed library containing an atomic block truth table, and compare the mentioned cuts with the atomic block truth table in the constructed library, wherein during a comparison, all the cuts are searched for, output vectors of the cuts are aligned with one output vector in the constructed library containing the atomic block truth table, and when an output vector displayed for a group of cuts with a common input is same as an output vector in the atomic block truth table in the constructed library, the group is identified as one atomic block; and
the adder tree recovery algorithm utilizes, based on a breadth-first search (BFS) method, some reserved adder boundaries that provide significant structural information; the adder tree recovery algorithm maintains a front queue (FQ) comprising an HA/an FA/an AND gate that generates/consumes an unexplored partial product, and the FQ is initialized as all AND gates of generating initial PPij′; the adder tree recovery algorithm also maintains a partial product map (PPM) from a weight Wk to an active partial product, and the PPM is initialized as PPM[Wk]={PPij}, k=i+j, wherein PPM[Wk] represents a mapping from the weight Wk to a partial product, and PPij represents a partial product generated after ith and jth bits of a multiplier pass through the AND gate; then, the adder tree recovery algorithm iteratively dequeues an atomic block from the FQ, stops using a consumed partial product, and adds the generated partial product to the PPM; then, the adder tree recovery algorithm fans out an adder type of the atomic block, wherein a fanin HA/FA of the atomic block has been processed and added to the FQ; and when the FQ is empty, the adder tree recovery algorithm terminates, an accessed HA/FA and a connection form a partial adder tree, and a remaining partial product in the PPM is required to be further processed;
step 2: reserving, for each weight Wk by the adder tree recovery algorithm, Rk partial products that are represented as PPM[Wk]={Pk,0 . . . Pk,Rk−1}, wherein 0≤k<2n, n represents a quantity of input bits of the multiplier, and Pk,Rk−1 represents an (Rk−1)th reserved partial product of the weight Wk; modeling a reconstructed PPA as a constraint satisfaction problem that is represented as an N-step planning process, wherein at each step, two decisions are made: whether to generate the FA/HA, and selection of an input of the FA/HA; a generated carry/sum is also used as an input of a subsequent FA/HA for tracking; and defining a selection matrix Sel and a state matrix State for each weight Wk, wherein
based on the selection matrix Sel and the state matrix State, architectural constraints are generated to represent a generation process, comprising an adder input selection constraint, a state constraint, a Final Stage Adder (FSA) constraint and an unresolved pin constraint, and the constraints are encoded into a constraint programming (CP)-SAT solver to generate a satisfiable solution; and the process comprises: starting from a small decision step, increasing a step size and re-adding the constraints until a solution is found or timeout occurs; and then, checking the selection matrix Sel to convert the solution into an actual PPA architecture, and generating Verilog code of the multiplier for verification; and
step 3: after generating Verilog code of a reference multiplier, converting the Verilog code into an AIG and performing verification by using an SCA-based method; then creating a miter AIG from the optimized multiplier and the reference multiplier, and accelerating verification of SAT of the miter AIG through SAT sweeping, wherein the process starts with simulation of the miter AIG using a random input vector, and identifies all potential equivalent internal nodes based on a simulation result; next, using a Kissat 3.0 SAT solver to verify whether the nodes are indeed equivalent, and based on verification results of all the potential equivalent nodes, confirming that the equivalent nodes are merged to simplify the miter AIG; and repeating the above process until the SAT of the miter AIG is determined, and outputting a counterexample diagnostic error if the miter AIG is satisfiable, or confirming correctness of the optimized multiplier if the miter AIG is not satisfiable.
|