Optical Computing in Formal Verification
Optical Computing in Formal Verification
Formal Verification in Integrated Circuit Design
In today’s technology landscape, integrated circuit (IC) design is both highly precise and extremely complex. Within the chip design flow, Electronic Design Automation (EDA) software plays a critical role, and among its many tasks, design verification is especially important. Verification checks whether a chip design is correct and secure, accounting for roughly half of the total cost and time of chip design. Formal verification uses formal proofs to verify whether a design functions correctly. It is a vital method for ensuring chip correctness and security and has become a key module in EDA software.
A major advantage of chip verification is that it can be performed early in the design phase, without the need to fabricate physical chips or carry out physical tests. This allows designers to find and fix problems before manufacturing, saving both time and cost. In addition, verification can help uncover errors that are difficult to detect through conventional simulation, thus improving design reliability.
However, formal verification also faces challenges. For complex circuit designs, it demands substantial computational resources and time. In recent years, IC scale has continued to grow and transistor counts have increased enormously. For instance, Apple’s dual-chip M1 Ultra SoC integrates 114 billion transistors, and Nvidia’s latest H100 chip contains 80 billion transistors. These scales pose new challenges to the computing power and runtime required for formal verification. Formal verification methods include equivalence checking and formal assertion-based verification. They are mainly solved using two approaches:
Binary Decision Diagrams (BDDs)
Propositional satisfiability (SAT) solving
The SAT Problem
The satisfiability problem (SAT) is a fundamental problem in computer science. It asks whether there exists an assignment of variables that makes a given Boolean logic formula true. Research on this problem dates back to the 1960s, when researchers began using computers to solve Boolean logic problems. SAT has been studied extensively in theoretical computer science and is applied in hardware and software verification, automated theorem proving, artificial intelligence, and optimization. In chip design, SAT solvers can verify whether a circuit satisfies a given specification. In software development, SAT can help locate program bugs or optimize code. By reducing a problem to SAT, one can leverage existing efficient algorithms and tools to find solutions. Research on the SAT problem has not only advanced computer science but also played a significant role across many practical domains.
In a SAT problem, we are generally given:
A set of variables, consisting of n variables {x₁, x₂, …, xₙ}, along with a set of 2n literals {x₁, ¬x₁, x₂, ¬x₂, …, xₙ, ¬xₙ}, where for variable xᵢ, xᵢ is a positive literal and ¬xᵢ is a negative literal.
A clause is a disjunction of some literals from the literal set; that is, each clause can be written as x₁ ∨ x₂ ∨ x₃ ⋯ , i.e., an OR of variables.
Conjunctive Normal Form (CNF): by taking the conjunction (AND) of m clauses c₁, c₂, …, cₘ, we can easily form a propositional formula in CNF: F = c₁ ∧ c₂ ∧ … ∧ cₘ.
A propositional logic formula can therefore be viewed as a pair consisting of a variable set and a clause set.
Clearly, every clause in a formula is in one of two states:
(1) satisfied
(2) unsatisfied
A clause is satisfied if and only if at least one of its literals evaluates to true under a truth assignment (since the literals in a clause are connected by OR, a satisfied clause means at least one variable in it is true under the initial assignment). The SAT problem is to determine, for a given CNF formula F, whether there exists a complete assignment that makes all clauses in F satisfied—that is, makes every clause true.
Currently, SAT solving algorithms can be broadly divided into two categories: complete algorithms and incomplete algorithms.
Complete algorithms, due to their exhaustive search techniques, can determine whether a SAT instance is satisfiable or unsatisfiable, but may not always deliver an answer within a reasonable time.
Incomplete algorithms, typically local search algorithms, can only determine satisfiability for a SAT instance, but they can do so very efficiently on satisfiable instances.
SAT in Formal Verification
Suppose we have a circuit design containing multiple logic gates and wires. We want to verify whether the design satisfies certain properties, such as safety, correctness, or performance requirements. To perform formal verification, we can reduce the problem to a SAT problem.
First, we construct a Boolean logic formula that describes the intended behavior of the circuit. This formula includes input variables, output variables, and the relationships among the logic gates. For instance, we can use Boolean expressions to state that the circuit output should take specific values under certain input conditions.
Next, we transform this Boolean formula into a SAT problem. A SAT problem asks whether there exists a variable assignment that makes a given Boolean formula true. We treat the circuit’s input variables as the variables of the SAT problem and turn the behavioral specification into a logical formula that serves as the input to the SAT problem.
Finally, we use a SAT solver to solve this SAT problem. The SAT solver attempts to find a variable assignment that satisfies the Boolean formula. If the SAT solver finds such an assignment, it means the circuit design meets the given behavioral specification. If the SAT solver fails to find a satisfying assignment, it returns an assignment that does not satisfy the formula. Such an assignment can help us identify problems in the design and guide further debugging and repair.
Optical Computing Algorithm for Solving SAT
The optical computing algorithm is designed to solve the SAT problems that arise from formal verification transformations.
Pre-processing
For a SAT problem with n variables and m clauses, we can represent it using an n × m matrix M. Each row of M indicates the position and sign of each variable in a clause. We also keep a length-m vector L that records the length of each clause. We then set the model’s threshold as T = 1 − L. The initial energy vector can be computed as: G = sign(M × S − T), where S is the state vector (Sᵢ = ±1). The advantage of this energy design is that a satisfied clause corresponds to an energy value of 1, and otherwise 0.
Optical asynchronous algorithm
Given the energy vector G, we can determine the satisfaction status of each clause under the current assignment (1 or 0). This helps us quickly locate unsatisfied clauses and update them, yielding faster convergence than Ising algorithms. The iterative steps of this optical computing-based asynchronous algorithm are as follows:
Randomly initialize a state vector S.
Compute the energy vector G = sign(M × S − T), averaging over multiple runs (can be accelerated by optical computing).
Record the lowest energy G and the corresponding state vector S.
Randomly select a clause C from the set of unsatisfied clauses.
For each variable σₖ in clause C, compute the energy Gₖ after flipping that variable, plus noise (can be accelerated by optical computing).
Pick the variable that yields the largest decrease in energy and update the state vector S accordingly.
If the best number of satisfied clauses is less than m and the maximum number of iterations has not been reached, return to step 2; otherwise, terminate and output the best state vector S found and the corresponding maximum number of satisfied clauses.
Step 5 can exploit the intrinsic noise of the optical computing chip to help the algorithm escape local optima.
Application Case
Lightelligence Joins Hands with X-Epic to Advance Strategic “Photonic Chip + EDA” Technology Development
Global leader in optoelectronic hybrid computing, Lightelligence, recently announced a collaboration with X-Epic, a system-level verification EDA solution provider, to pursue forward-looking strategic R&D in “photonic chip + EDA.” The two companies will conduct joint research on heterogeneous acceleration for EDA, leveraging the acceleration capabilities of photonic chips, and will build an integrated hardware-software optoelectronic hybrid turnkey solution to meet the growing data processing and computing demands in areas such as big data and artificial intelligence.
Traditional electronic chips are gradually becoming unable to meet the increasing requirements for performance speedup and data transmission alongside energy efficiency demands. Photonic chips, with their high throughput, low latency, and low power consumption, can effectively boost the speed and bandwidth of electronic integrated devices. As a result, optoelectronic hybrid computing has emerged as an effective way to break through current IC design bottlenecks.
Zhonghui Xie, Chief Marketing Strategy Officer of X-Epic and Executive Deputy Dean of X-Epic Research Institute, said: “The photonic chip market is growing rapidly and will bring tremendous changes to many industries, creating exciting new opportunities for future digital development. By building on Lightelligence’s advanced optical computing and optical networking technologies, we will fully harness the potential of optoelectronic hybrid computing, usher in a new era of accelerated verification computing power for EDA, and further enhance the computation efficiency of X-Epic’s system-level verification tools. Through in-depth cooperation with Lightelligence, we will actively explore the photonic chip verification field, accelerate photonic chip development, and provide a solid foundation for the high-quality growth of the digital economy.”
