Preserving Design Hierarchy Information for Polynomial Formal Verification
Preserving Design Hierarchy Information for Polynomial Formal Verification
复制标题
保留多项式形式验证的设计层次结构信息
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Alireza Mahzoon
中科院分区：
文献类型：
--
作者：
R. Drechsler;Alireza Mahzoon
随着数字电路的日益复杂，为保证电路的正确性，形式验证已成为设计后的一项重要任务。许多现有的验证方法在性能上存在不可预测性。不清楚它们是否必须运行数秒、数小时或数天才能返回验证结果，或者它们最终是否失败。不可预测性只能通过确保复杂性界限来解决。为了保证可扩展性，我们对多项式形式验证（PFV）特别感兴趣，其中空间和时间复杂性相对于电路的大小具有多项式界。关于设计层次结构的信息通常对PFV至关重要。复杂的数字电路由多个组件组成，无法用多项式空间和时间的单个验证技术进行验证。然而，随着对组件边界的额外了解，通过对子组件的逐步验证和使用不同的形式证明引擎，PFV成为可能。本文首先介绍了PFV并阐明了它的重要性。我们考虑了几种扁平化门级算术电路的验证，并说明了当没有设计层次可用时，PFV的挑战。然后，我们将展示如何通过保留设计层次结构信息（包括组件的边界）来克服这些挑战。
With the growing complexity of digital circuits, formal verification has become a crucial task after the design in order to ensure the correctness of a circuit. Many existing verification methods suffer from unpredictability in their performance. It is not clear whether they have to be run for seconds, hours, or days to return the verification results or whether they fail in the end. The unpredictability can only be resolved by ensuring complexity bounds. To guarantee scalability we are in particular interested in Polynomial Formal Verification (PFV), where the space and time complexities have polynomial bounds with respect to the size of the circuit.The information about the design hierarchy is usually vital for PFV. Complex digital circuits consist of several components that cannot be verified with an individual verification technique in polynomial space and time. However, with additional knowledge about the boundaries of components, PFV becomes possible through the step-wise verification of sub-components and the use of different formal proof engines. In this paper, we first introduce PFV and clarify its importance. We consider the verification of several flattened gate-level arithmetic circuits and illustrate the challenges of PFV when no design hierarchy is available. Then, we show how these challenges can be overcome by preserving design hierarchy information including the boundaries of the components.