A Library for Combinational Circuit Verification Using the HOL Theorem Prover

作者：Shiraz Sumayya; Hasan Osman^*

来源：IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2018, 37(2): 512-516.

DOI：10.1109/TCAD.2017.2705049

• combinational circuits
• formal verification

Interactive theorem provers can overcome the scalability limitations of model checking and automated theorem provers by verifying generic circuits and universally quantified properties but they require explicit user guidance, which makes them quite uninteresting for industry usage. As a first step to overcome these issues, this paper presents a formally verified library of commonly used combinational circuits using the higher-order logic theorem prover HOL4. This library can in turn be used to verify the structural view of any arbitrary combinational circuit against its behavior with very minimal user-guidance. For illustration, we verified several combinational circuits, including a 24-bit adder/subtractor, the 8-bit shifter module of the c3540 benchmark, the 17-bit EqualZ_W module of the c2670 benchmark, a 16:1 Multiplexer, and a 512-bit Multiplier.

• 出版日期2018-2