Design and Verification of Speed-Independent Circuits with Arbitration in Workcraft
Design and Verification of Speed-Independent Circuits with Arbitration in Workcraft
复制标题
DOI：
10.1109/async.2018.00017
复制
发表时间：
2018-05
期刊：
影响因子：
--
通讯作者：
D. Sokolov;Victor Khomenko;A. Yakovlev;D. Lloyd
中科院分区：
文献类型：
--
作者：
D. Sokolov;Victor Khomenko;A. Yakovlev;D. Lloyd
传统的速度无关(SI)电路设计方法要求其行为是输出持久的。非持续性的一个常见来源是导致在输出信号之间进行选择的仲裁。设计者有责任在继续进行综合之前删除这种非持久性行为，通常是通过手动将仲裁分解到环境中，在环境中使用互斥元素实现选择。这种方法有几个问题：大量的手动工作，分离出互斥锁，并在合成后插入它。不能保证设计者认为可以由互斥锁实现的信号实际上遵循仲裁协议。因式分解将互斥锁授权转换为输入，因此输出持久性的验证将错过由于过早撤回相应请求而禁用互斥锁授权的情况(这适用于对原始规范和电路实现的验证)。在这篇文章中，我们演示了如何通过将自动互斥锁插入集成到在https://workcraft.org/).中实现的SI综合流程中来解决这些问题
The traditional design methods for speed-independent (SI) circuits require their behaviour to be output-persistent. A common source of non-persistence is arbitration that leads to a choice between output signals. It is the designer's responsibility to remove such non-persistent behaviour before proceeding to synthesis, usually by manually factoring the arbitration out into the environment, where the choice is implemented using a mutex element. There are several problems with this approach: Significant manual effort factoring out the mutex and inserting it after synthesis. There is no guarantee that the signals the designer thinks can be implemented by a mutex actually follow the arbitration protocol. Factoring out converts mutex grants into inputs, so verification of output-persistence would miss a situation when a mutex grant is disabled due to premature withdrawal of the corresponding request (this applies to verification of both, the original specification and the circuit implementation). In this paper we demonstrate how these problems were solved by integrating automatic mutex insertion into the SI synthesis flow implemented in Workcraft (https://workcraft.org/).