去同步设计中流等价性的形式化验证
计算机科学中的逻辑
2020-04-23 v1
摘要
Cortadella、Kondratyev、Lavagno 与 Sotiriou 的开创性工作包含一份手写证明，表明某特定握手协议保持流等价性——一种同步锁存器规范与其去同步捆绑数据异步实现之间的等价性概念。在本工作中，我们指出了 Cortadella 等人证明的一个反例，说明了他们的协议实际上如何导致对流等价性的违反。然而，他们论文中提出的两种并发性较弱的协议确实保持了流等价性。为验证这一事实，我们在 Coq 证明助手中形式化了流等价性，并给出了我们结果的机械化、机器可检查证明。
引用
@article{arxiv.2004.10655,
title = {Formal Verification of Flow Equivalence in Desynchronized Designs},
author = {Jennifer Paykin and Brian Huffman and Daniel M. Zimmerman and Peter A. Beerel},
journal= {arXiv preprint arXiv:2004.10655},
year = {2020}
}
备注
To appear in ASYNC 2020