Research on Development of Logic Synthesizer and Design Verifier for Sequential Circuits Based on Boolean Function Manipulation

本文对基于布尔函数操作的时序电路逻辑综合器和设计验证器的研制进行了如下研究：1。基于布尔函数操作的时序电路逻辑综合器针对异步时序电路的单次状态分配和单跳变时间分配问题，提出并实现了基于布尔函数操作的最小解算法.基于布尔函数操作的时序电路设计验证器我们提出了一种基于布尔函数操作的设计验证算法，该算法采用分支时间规则时序逻辑（BRTL）作为规范语言，与传统时序逻辑相比，BRTL具有更高的表达能力。基于该算法，我们开发了一个设计验证器，并成功应用于微处理器的设计验证.有效的布尔函数操作我们阐明了共享二叉决策图（SBDD）操作布尔函数的理论性质。我们还提出并实现了一个寻找输入变量排序的算法，使得图变小，并有效地处理二级存储上的大容量SBDD.逻辑综合器和设计验证器的图形界面我们在工作站上利用X窗口系统实现了多机多屏系统，实现了高分辨率和高速绘图。

We carried out Research on development of logic synthesizer and design verifier for sequential circuits based on Boolean function manipulation as follows:1. Logic synthesizer for sequential circuits based on Boolean function manipulationFor one-shot state assignment and single transition time assignment for asynchronous sequential circuits, we have proposed and implemented algorithms of finding minimum solutions based on Boolean function manipulation.2. Design verifier for sequential circuits based on Boolean function manipulationWe have proposed a design verification algorithm based on Boolean function manipulation, which assumes, as a specification language, branching time regular temporal logic (BRTL), which has higher expressive power as compared with the conventional temporal logics. We have developed a design verifier based on the algorithm and succeeded in design verification of microprocessors.3. Efficient Boolean function manipulationWe have clarified the theoretical properties of shared binary decision diagram (SBDD) to manipulate Boolean functions. We also have proposed and implemented an algorithm of finding input variable ordering such that the diagram becomes small and an algorithm to deal with SBDD of large size on secondary storage efficiently.4. Graphic interface of logic synthesizer and design verifierWe have implemented a multi-computer multi-screen system by using the X window system on workstations and achieved high resolution and high-speed drawing.