qMC: A Formal Model Checking Verification Framework For Superconducting Logic
qMC: A Formal Model Checking Verification Framework For Superconducting Logic
复制标题
qMC：超导逻辑的形式化模型检查验证框架
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Shahin Nazarian
中科院分区：
文献类型：
--
作者：
Mustafa Munir;Aswin Gopikanna;A. Fayyazi;M. Pedram;Shahin Nazarian
单通量量子（SFQ）电路作为超导电子学（SCE）的一个例子，具有取代CMOS电路的潜力，因为它们具有功率降低三个数量级的理论潜力，伴随着一个数量级的更高速度。尽管SCE社区有很多好处，但它缺乏一个可靠的开源正式验证解决方案。本文提出了一个验证框架称为qMC，SFQ电路的模型检查器使用形式化技术。qMC提供了一个自动化的过程，构建一个SystemVerilog测试平台，包括正式的断言，以验证SFQ特定的电路属性，并使用模型检查（MC）产生系统的正确性结果和反例。我们没有从头开始创建MC工具，而是基于成熟的CMOS电路MC开源后端验证引擎（包括Yosys-SMTBMC和EBMC）构建了qMC。qMC允许在SystemVerilog形式断言、时间限制SystemVerilog断言或线性时序逻辑（LTL）中给出属性。与最先进的基于SFQ的半正式验证框架相比，qMC在验证时间和覆盖率方面有所改进。例如，4位阵列乘法器的验证时间加快了19.5倍。
Single flux quantum (SFQ) circuits as an example of superconducting electronics (SCE) have the potential to replace CMOS circuits as they possess a theoretical potential of three orders of magnitude reduction in power accompanied with one order of magnitude higher speed. Despite its benefits, the SCE community lacks a reliable open source formal verification solution. This paper proposes a verification framework called qMC, a model checker for SFQ circuits using formal techniques. qMC offers an automated process that constructs a SystemVerilog testbench consisting of formal assertions to verify the SFQ-specific properties of the circuits and produce system correctness results and counterexamples using model checking (MC). Instead of creating an MC tool from scratch, we have built qMC based on well established open source back-end verification engines for MC of CMOS circuits, including Yosys-SMTBMC and EBMC. qMC allows for properties to be given in SystemVerilog formal assertions, time-limited SystemVerilog assertions, or linear temporal logic (LTL). qMC provides an improvement in terms of verification time and coverage when compared to state-of-the-art semi-formal based SFQ verification frameworks. For instance, verification time for a 4-bit array multiplier is sped up by 19.5x.