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

数据通道电路采用双轨编码是异步电路设计的主要方法之一。这种方法需要大量的C元件，这是存储设备，在控制电路，它会导致一些问题，在综合和验证，如状态空间的增加，性能下降，等等，因此，本项目提出使用三轨编码代替双轨编码实现电路没有C元件。实际上，我们已经选择了一个三进制码这样的三轨编码，并开发了两个程序，以获得基本的三进制门从给定的真值表的基础上的三进制码。另一方面，当我们要验证一个包含数据通路的异步电路时，我们通常会对电路进行抽象，去除大部分的数据通路。这是因为在没有抽象的情况下验证电路需要检查数据路径所采用的整个数据值，这使得描述规范和遍历其巨大的状态空间变得非常困难。本项目还提出了使用一些特定的或随机的值来部分地验证数据路径，并像往常一样形式化地验证控制部分。这使我们能够在不进行抽象的情况下对给定电路进行验证，这仍然为我们提供了相当可靠的结果。为此，我们扩展了现有的模型（时间Petri网），使其可以处理生产和比较数据。此外，为了避免扩展时间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.