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.