论文标题
在异步设计中的流量等效性的形式验证
Formal Verification of Flow Equivalence in Desynchronized Designs
论文作者
论文摘要
Cortadella，Kondratyev，Lavagno和Sotiriou的开创性作品包括手写证据，表明特定的握手协议可以保留流量等效性，这是基于同步闩锁的规格与其脱离串联捆绑的捆绑数据和同步的data asynChronous实现之间的等效概念。在这项工作中，我们确定了Cortadella等人的证明的反例，说明了他们的协议实际上如何导致违反流量对等。但是，在其论文中确定的两个较不同时的协议确实保留了流量等效性。为了验证这一事实，我们将COQ证明助手中的流量等效正式化，并提供了机械化的，可靠的结果证明我们的结果。
Seminal work by Cortadella, Kondratyev, Lavagno, and Sotiriou includes a hand-written proof that a particular handshaking protocol preserves flow equivalence, a notion of equivalence between synchronous latch-based specifications and their desynchronized bundled-data asynchronous implementations. In this work we identify a counterexample to Cortadella et al.'s proof illustrating how their protocol can in fact lead to a violation of flow equivalence. However, two of the less concurrent protocols identified in their paper do preserve flow equivalence. To verify this fact, we formalize flow equivalence in the Coq proof assistant and provide mechanized, machine-checkable proofs of our results.
