Equivalence verification for NULL Convention Logic (NCL) circuits
Equivalence verification for NULL Convention Logic (NCL) circuits
复制标题
NULL 约定逻辑 (NCL) 电路的等效性验证
DOI：
10.1109/iccd.2014.6974681
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
S. Smith
中科院分区：
文献类型：
--
作者：
Vidura Wijayasekara;S. Srinivasan;S. Smith
空约定逻辑 (NCL) 电路是异步电路，由于其对延迟不敏感的特性而在 SoC 设计中得到应用，这使得可以轻松解决 SoC 的 IP 组件重用中的时序问题。 NCL 组件通常由同步电路合成。对于任何可行的设计范例，验证是一个重要因素。我们提出了一种正式的验证方法，用于检查 NCL 电路与其同步父电路的等效性。该方法包括计算 NCL 时序电路的可达状态的过程和可用于将 NCL 电路状态映射到同步电路状态的细化映射函数。通过验证几个 NCL 电路的正确性来证明该方法。
NULL Convention Logic (NCL) circuits are asynchronous circuits and find application in SoC design due to their delay-insensitive nature, which allows ease in resolution of timing issues in IP component reuse for SoC. NCL components are typically synthesized from synchronous circuits. For any design paradigm to be feasible, verification is an important factor. We present a formal verification methodology for checking equivalence of NCL circuits against their synchronous parent circuits. The methodology includes a procedure that computes the reachable states of NCL sequential circuits and a refinement mapping function that can be used to map NCL circuit states onto synchronous circuit states. The methodology is demonstrated by verifying the correctness of several NCL circuits.