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.