Formal Verification of Mixed-Signal Systems Using Real Number Modeling with SMT-based Model Checking

Abstract

Formal verification of digital hardware designs is a well established practice in the semiconductor industry. However, designs combining digital and analog components (mixed-signal designs) remain with limited application of formal verification due to the complexity of automating proofs on the continuous state space of analog systems. In this work we perform a case study of formal verification for mixed-signal designs where we instrumentalize Yosys, an industrial-grade SystemVerilog compiler, and Pono, a state-of-the-art word-level model checker, to implement a formal verification flow on a set of 31 realistic mixed-signal benchmarks that we crafted from testbenches for analog blocks using real number modeling. As the practice of abstracting the analog domain with real-valued variables in SystemVerilog is already common place on simulation, we propose an interpretation of such verification problems on the theory of real arithmetic, which enables order of magnitude verification speed-ups using SMT solvers relative to the traditional bit-blasting interpretation on the theory of floating-point arithmetic. Despite the semantic differences between the two theories, our benchmarks indicate that mixed-signal hardware verification problems are not dependent on floating-point arithmetic details in practice, which favors the adoption of real arithmetic solvers. To demonstrate the practicality of this method, we perform a comparative analysis of the results from different theories over our benchmark set and discuss the technical trade-offs that arise when introducing formal verification to the mixed-signal verification domain.