Quantum Equivalence Checking. Innovation in Verification

Source: https://semiwiki.com/eda/372999-quantum-equivalence-checking-innovation-in-verification/

Can quantum computing have any relevance to EDA? This month’s paper suggests it might have a role someday, in accelerating one of the most fundamental of EDA algorithms: SAT. Paul Cunningham (GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and lecturer at Stanford, EE292A) and I continue our series on research ideas. As always, feedback welcome.

양자 컴퓨팅이 EDA(전자 설계 자동화)와 어떤 관련이 있을까요? 이번 달의 논문은 양자 컴퓨팅이 언젠가 EDA의 가장 근본적인 알고리즘 중 하나인 SAT(만족도가능성 문제)를 가속화하는 데 역할을 할 수도 있음을 시사합니다. 케이던스(Cadence)의 검증 총괄 제너럴 매니저인 폴 커닝햄(Paul Cunningham), 실리콘 캣리스트(Silicon Catalyst)의 창업자이자 전 시놉시스 CTO 겸 스탠퍼드대학교(EE292A) 강사인 라울 캄포사노(Raúl Camposano), 그리고 저 이렇게 세 사람이 연구 아이디어에 관한 시리즈를 이어갑니다. 언제나 피드백은 환영합니다.

The Innovation

This month’s pick is qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking. The authors are from Cyber-Physical Systems, Siemens EDA, and University of Bremen, all in Germany. The paper (2024) has been published in the ACM Journal on Emerging Technologies in Computing Systems and has 6 citations.

이번 달의 선정작은 qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking(하드웨어 동등성 검증을 위한 효율적인 양자 만족도가능성 해법 설계)입니다. 저자들은 모두 독일의 사이버-물리 시스템(Cyber-Physical Systems), 지멘스 EDA(Siemens EDA), 브레멘 대학교(University of Bremen) 소속입니다. 이 논문은 (2024년) ACM Journal on Emerging Technologies in Computing Systems에 출판되었으며 6회의 인용 횟수를 기록하고 있습니다.

SAT is foundational in multiple EDA algorithms, in verification and synthesis, and is the standard benchmark for algorithm complexity. What better challenge then for quantum computing which aims to deliver (at least in some cases) exponential speedup over classical computing methods?

SAT(만족도가능성 문제)는 검증 및 합성 분야의 여러 EDA 알고리즘에서 핵심적인 역할을 하며, 알고리즘 복잡도의 표준 벤치마크입니다. 고전 컴퓨팅 방식에 비해 (일부 경우에 한해서라도) 지수 함수적 속도 향상을 목표로 하는 양자 컴퓨팅에 이보다 더 좋은 도전 과제가 어디 있을까요?

Logic circuit examples considered in this paper are very elementary – multiplexers and 1-bit full adders for example, testing first basic viability of the method. Tests have been run on IBM quantum computers with an initial focus on resources – how many qubits are required and quantum circuit depth, rather than on performance.

이 논문에서 다룬 논리 회로 예제들은 멀티플렉서와 1비트 전가산기(Full Adder) 등 매우 기초적인 수준으로, 해당 방법론의 기본적인 실현 가능성을 우선적으로 테스트했습니다. 실험은 IBM 양자 컴퓨터에서 수행되었으며, 성능보다는 성능 저하 요인인 자원(필요한 큐비트 수와 양자 회로의 깊이)에 초점을 맞췄습니다.

Paul’s view

Back to quantum computing this month. Last time we blogged on building a quantum simulator, this time it’s on building a quantum formal equivalence checker. At its heart, formal equivalence is a Boolean satisfiability (SAT) problem: XOR the spec with the implementation and any solution must be a situation where the spec and implementation differ.

이번 달에는 다시 양자 컴퓨팅으로 돌아왔습니다. 지난번에는 양자 시뮬레이터 구축에 관해 블로그에 글을 썼다면, 이번에는 양자 형식적 동등성 검증기(quantum formal equivalence checker) 구축에 관한 내용입니다. 그 핵심에서 형식적 동등성은 불리언 만족도가능성(SAT) 문제입니다. 사양(Spec)과 구현(Implementation)을 XOR 연산하면, 그 어떤 해법도 사양과 구현이 서로 다른 상황을 가리켜야 합니다.

Commercial SAT on a classical computer begins by converting a circuit or spec into Conjunctive Normal Form (CNF), which can be done quickly and efficiently using the Tseytin method. Many fast, parallelizable algorithms exist to search heuristically over a CNF to find a variable assignment that satisfies it, for example Kissat.

고전 컴퓨터에서의 상용 SAT는 회로 또는 사양을 CNF(Conjunctive Normal Form, 연역적 표준형)로 변환하는 것으로 시작하며, 이는 체이틴(Tseytin) 방법을 통해 빠르고 효율적으로 수행될 수 있습니다. Kissat과 같이 CNF를 휴리스틱하게 탐색하여 이를 만족하는 변수 할당을 찾는 빠르고 병렬화 가능한 많은 알고리즘이 존재합니다.

To implement a Boolean expression in a quantum circuit, it is best to represent the expression with XOR and AND functions, since the fundamental building block of Boolean expressions in a quantum circuit is the Toffoli gate, which implements the expression “a XOR (b AND c)”.

양자 회로에서 불리언 표현을 구현하려면, 양자 회로 내 불리언 표현의 근본적인 구성 요소가 “a XOR (b AND c)”를 구현하는 토폴리 게이트(Toffoli gate)이므로, 해당 표현을 XOR 및 AND 함수로 나타내는 것이 가장 좋습니다.

The main contribution in this paper is set of expression rewriting rules that improve the efficiency of mapping a Tseytin CNF into Toffoli gates, while still being fast and memory efficient to apply. On some very small 3-input circuits (like a mux or adder) these rules reduce the total number of quantum gates in the authors’ quantum SAT solver by over 2x.

이 논문의 주요 기여는 체이틴 CNF를 토폴리 게이트로 매핑하는 효율성을 향상시키는 동시에 적용하기에 빠르고 메모리 효율적인 일련의 표현 재작성 규칙들입니다. 저자들은 멀티플렉서나 가산기와 같은 일부 매우 작은 3입력 회로에서 이 규칙들이 양자 SAT 솔버 내의 총 양자 게이트 수를 2배 이상 줄여준다고 밝혔습니다.

The actual solving part of the authors’ method uses Grover’s Algorithm. This algorithm is beyond our blog but is seriously innovative and cool. Executive summary: a SAT solver on a classical computer is O(2^n) for n boolean variables.  Grover’s algorithm on a quantum computer is O(2^(n/2)), so a quadratic factor more efficient.

저자들 방식의 실제 풀이 파트는 그로버 알고리즘(Grover’s Algorithm)을 사용합니다. 이 알고리즘은 저희 블로그의 범위를 넘어서지만 대단히 혁신적이고 멋진 기술입니다. 요약하자면, 고전 컴퓨터의 SAT 솔버는 n개의 불리언 변수에 대해 O(2^n)의 복잡도를 가지지만, 양자 컴퓨터의 그로버 알고리즘은 O(2^(n/2))이므로 이차(quadratic) 인자만큼 더 효율적입니다.

But don’t get too excited yet – modern SAT solvers routinely solve expressions with millions of variables in only minutes. Current quantum computers can SAT solve less than 100 variables.

하지만 아직 너무 흥분하지는 마십시오. 현대의 SAT 솔버들은 단 몇 분 만에 수백만 개의 변수를 가진 표현을 일상적으로 풀어냅니다. 반면 현재의 양자 컴퓨터는 100개 미만의 변수에 대해서만 SAT를 풀 수 있습니다.

Raúl’s view

SAT was the first problem proven to be NP-complete: every problem in NP can be reduced to SAT. It also has numerous applications in digital circuit design, including optimization and verification. Quantum computing does not make SAT fundamentally easier, SAT remains an NP-complete problem, but it can speed up the search for solutions. For example, Grover’s algorithm provides a quadratic speedup, reducing a brute-force search over (2ⁿ) assignments from (O(2ⁿ)) to (O(2^n/2)). This paper introduces qSAT, a quantum SAT solver based on Grover search, and develops an end-to-end framework for applying it to Boolean equivalence checking in hardware verification. The authors describe it, “to the best of our knowledge,” as a first attempt toward a complete qSAT solver on a quantum computer.

SAT는 NP-완전(NP-complete) 문제로 증명된 최초의 문제였습니다. NP에 속하는 모든 문제는 SAT로 환원될 수 있습니다. 또한 SAT는 최적화 및 검증을 포함한 디지털 회로 설계에서 수많은 응용 분야를 가지고 있습니다. 양자 컴퓨팅이 SAT를 근본적으로 더 쉽게 만들어주는 것은 아닙니다. SAT는 여전히 NP-완전 문제로 남지만, 해를 찾는 탐색 과정을 가속화할 수는 있습니다. 예를 들어, 그로버 알고리즘은 이차적 속도 향상을 제공하여 2ⁿ개의 할당에 대한 브루트 포스(전수조사) 탐색을 O(2ⁿ)에서 O(2^n/2)로 줄여줍니다. 본 논문은 그로버 탐색을 기반으로 하는 양자 SAT 솔버인 qSAT를 소개하고, 이를 하드웨어 검증의 불리언 동등성 검증에 적용하기 위한 엔드투엔드 프레임워크를 개발했습니다. 저자들은 이를 “우리가 아는 한” 양자 컴퓨터 상에서 완전한 qSAT 솔버를 구현하려는 최초의 시도라고 설명합니다.

Notes: 1) Other approaches to implementing SAT on quantum computers include Quantum Annealing, the Quantum Approximate Optimization Algorithm (QAOA), etc.

2) This paper’s “qSAT” should not be confused with QSAT / Quantum Satisfiability, the QMA-complete quantum analogue of SAT (QMA, Quantum Merlin-Arthur, is the quantum analogue of classical NP).

참고 사항:

1. 양자 컴퓨터에서 SAT를 구현하는 다른 접근 방식으로는 양자 어닐링(Quantum Annealing), 양자 대략적 최적화 알고리즘(QAOA) 등이 있습니다.
2. 이 논문의 “qSAT”는 SAT의 QMA-완전 양자 유사체인 QSAT / Quantum Satisfiability(QMA, Quantum Merlin-Arthur는 고전적 NP의 양자 유사체임)와 혼동되어서는 안 됩니다.

In their approach, a Boolean formula is rewritten in ESOP form (Exclusive Sum Of Products), because ESOP expressions map efficiently into reversible quantum circuits using controlled-X/Toffoli-type gates. These circuits are assembled into a quantum miter (the XOR of the outputs of the two circuits to be checked); the miter is then used as the oracle in Grover’s algorithm, marking input assignments that are counterexamples to equivalence.

이들의 접근 방식에서 불리언 공식은 ESOP(Exclusive Sum Of Products, 배타적 곱의 합) 형태로 재작성되는데, 이는 ESOP 표현이 제어-X/토폴리 계열 게이트를 사용하여 가역 양자 회로(reversible quantum circuits)로 효율적으로 매핑되기 때문입니다. 이 회로들은 양자 마이터(quantum miter, 검증할 두 회로 출력의 XOR)로 조립되며, 이 마이터는 그로버 알고리즘에서 오라클로 사용되어 동등성의 반례인 입력 할당을 마킹합니다.

The improvement is mainly in quantum resource usage. By utilizing compact ESOP representations and eliminating auxiliary variables, the authors reduce qubit counts, Grover iterations, gates, and circuit depth. For their larger examples, MUX and CARRY show about 27% fewer qubits and roughly 70% fewer gates and depth; the Full Adder shows about 20% fewer qubits and a 70% reduction in gates and depth. However, these metrics only compare their optimized formulation against their own less-optimized baseline. The paper does not provide a quantitative comparison against a prior independent quantum SAT solver.

개선 사항은 주로 양자 자원 사용량에 집중되어 있습니다. 컴팩트한 ESOP 표현을 활용하고 보조 변수를 제거함으로써, 저자들은 큐비트 수, 그로버 반복 횟수, 게이트 수, 그리고 회로 깊이를 줄였습니다. 더 큰 규모의 예제인 MUX와 CARRY의 경우 약 27% 적은 큐비트와 대략 70% 적은 게이트 및 깊이를 보여주었습니다. 전가산기(Full Adder)는 약 20% 적은 큐비트와 게이트 및 깊이에서 70% 감소를 기록했습니다. 그러나 이러한 측정치는 최적화된 공식을 자신들의 덜 최적화된 기준선(baseline)과 비교한 것에 불과합니다. 이 논문은 이전의 독립적인 양자 SAT 솔버와의 정량적인 비교는 제공하지 않습니다.

The paper is difficult to read because of non-standard English and a somewhat confusing organization. For example, it introduces the final quantum miter architecture before explaining the core ESOP mathematics needed to build it. The paper is also not very careful with notation. In Eq. (25), U= ϕ∧(ϕ⇔GR) is a Boolean expression. In Fig. 10, however, U is used for the measured probability of the expected outcome of the quantum implementation of U. The authors use “fidelity” loosely for the probability that the implemented circuit produces the expected output. They reuse ϕ, previously the output of the miter, and restrict the test to the case ϕ =1. They conclude that in almost all examples their smaller implementation also produces the expected output more reliably (Fig. 10). That is their “fidelity”.

이 논문은 표준에 어긋나는 영어 표현과 다소 혼란스러운 구성 때문에 읽기가 어렵습니다. 예를 들어, 그것을 구축하는 데 필요한 핵심 ESOP 수학을 설명하기 전에 최종 양자 마이터 아키텍처를 먼저 소개합니다. 또한 표기법 면에서도 아주 치밀하지는 않습니다. 식 (25)에서 U= ϕ∧(ϕ⇔GR)은 불리언 표현입니다. 하지만 그림 10에서는 $U$가 $U$의 양자 구현에서 예상되는 결과의 측정된 확률을 나타내는 데 사용됩니다. 저자들은 구현된 회로가 예상 출력을 생성할 확률을 의미하는 용어로 “충실도(fidelity)”를 대충 사용합니다. 그들은 이전에 마이터의 출력이었던 ϕ를 재사용하고, 테스트를 ϕ=1인 경우로 제한합니다. 그리고 거의 모든 예제에서 더 작은 구현이 예상 출력을 더 안정적으로 생성한다고 결론짓습니다(그림 10). 그것이 바로 그들의 “충실도”입니다.

As for what an actual IBM quantum computer can handle, even these examples are large: MUX requires about 1,000–3,400 CX gates and the full adder about 5,000–16,000. The IBM Grover tutorial notes that the number of sequential layers of two-qubit gates “grows extremely rapidly with the number of qubits — roughly exponentially, making Grover impractical on current noisy quantum hardware beyond very small problem sizes”. On today’s IBM hardware, the theoretical quadratic algorithmic speedup is overwhelmed by circuit depth and noise. Indeed, the complete qSAT/Grover circuits in the paper are evaluated on the ideal Aer simulator; the experiments on the actual IBM quantum computer are limited to the much smaller reference-model circuits used for the fidelity comparison.

실제 IBM 양자 컴퓨터가 처리할 수 있는 수준에 대해 말하자면, 이러한 예제들조차도 큽니다. MUX는 약 1,000-3,400개의 CX 게이트가 필요하며, 전가산기는 약 5,000-16,000개가 필요합니다. IBM 그로버 튜토리얼에서는 2큐비트 게이트의 순차적 레이어 수가 “큐비트 수에 따라 극도로 빠르게, 대략 지수 함수적으로 증가하여, 매우 작은 문제 크기를 넘어서는 현재의 노이즈가 있는 양자 하드웨어에서 그로버를 비실용적으로 만든다”고 지적하고 있습니다. 오늘날의 IBM 하드웨어에서는 이론적인 이차적 알고리즘 가속화 효과가 회로 깊이와 노이즈에 의해 압도당하고 맙니다. 실제로 논문 속 완전한 qSAT/Grover 회로는 이상적인 Aer 시뮬레이터에서 평가되었으며, 실제 IBM 양자 컴퓨터에서의 실험은 충실도 비교에 사용된 훨씬 더 작은 레퍼런스 모델 회로로 제한되었습니다.

Nevertheless, the paper makes a useful contribution to quantum formal verification: it shows how logic representation, specifically ESOP-based encoding, can substantially reduce the quantum resources required to implement a Grover-based equivalence checker.

그럼에도 불구하고 이 논문은 양자 형식적 검증에 유용한 기여를 합니다. 논리는 논리 표현, 구체적으로 ESOP 기반 인코딩이 그로버 기반 동등성 검증기를 구현하는 데 필요한 양자 자원을 실질적으로 줄일 수 있음을 보여줍니다.