Research on a synthesis and verification tool for high performance asynchronous circuits

对数据路径电路使用双轨编码是异步电路设计的主要方法之一。这种方法需要在控制电路中使用大量的存储器件C元件，在综合和验证中会出现状态空间增大、性能下降等问题。因此，本项目提出用三轨编码代替双轨编码来实现无C元件的电路。实际上，我们已经为这种三进制码选择了三进制码，并开发了两个程序来从给定的真值表中获得基于三进制码的基本三进制门。另一方面，当我们要验证一个包含数据路径的异步电路时，我们通常会对电路进行抽象，以删除大部分数据路径。这是因为在没有抽象的情况下验证电路需要检查数据路径采用的整个数据值，这使得描述规范和遍历其巨大的状态空间太困难了。本项目还提出使用特定的或随机的值对数据路径进行部分验证，并像往常一样对控制部分进行形式化验证。这允许我们在不抽象的情况下对给定电路进行验证，这仍然给我们提供了相当可靠的结果。为此，我们对现有的模型(时间Petri网)进行了扩展，使其能够处理产生和比较数据。此外，为了避免状态爆炸问题，针对这种扩展时间的Petri网，提出了一种能有效剪除验证和综合不必要的状态空间的偏序降阶算法。根据几个基准电路，已经发现它的性能优于基于现有模型的验证器。

Using dual-rail coding for data-path circuits is one of the major approaches for asynchronous circuit design. This approach requires a lot of C elements, which are memory devices, in control circuits, and it causes several problems in synthesis and verification, such as increase of state spaces, degradation of performance, and so on. Thus, this project proposes using three-rail coding instead of dual-rail coding to implement circuits without C elements. Actually, we have selected a ternary code for such the three-rail coding, and have developed two procedures to obtain basic ternary gates from given truth tables based on the ternary code. Furthermore, some optimization technique has also been developed.On the other hand, when we want to verify an asynchronous circuit including data-paths, we usually do the abstraction of the circuit to remove most of those data-paths. This is because verifying the circuit without abstraction requires checking the whole data values that the data-paths take, and this makes it too difficult to describe specifications and traverse its huge state space. This project also proposes to verify data-paths partially using some specific or random values with verifying the control parts formally as usual. This allows us to do the verification of a given circuit without abstraction which still gives us rather reliable results. For this purpose, we have extended the existing model (a time Petri net) such that it can handle producing and comparing data. In addition, in order to avoid the state explosion problem, a partial order reduction algorithm, which can efficiently prune away the state spaces unnecessary for the verification and synthesis, for such an extended time Petri net has been developed. According to several benchmark circuits, it has been found to outperform a verifier based on the existing model.