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

基于布尔函数操作的时序电路逻辑综合器和设计验证器的开发研究

• 批准号: 03555074
• 负责人: YAJIMA Shuzo
• 金额: $ 5.31万
• 依托单位: KYOTO UNIVERSITY
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Developmental Scientific Research (B)
• 财政年份: 1991
• 资助国家: 日本
• 起止时间: 1991 至 1992
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-03555074/
• 关键词: logic synthesis; logic design verification; sequential circuits; logic function optimization; state assignment; temporal logic; computer-aided logic design

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.

1.基于布尔函数运算的时序电路逻辑综合器针对异步时序电路的一次状态分配和单过渡时间分配，提出并实现了基于布尔函数运算的求最小解的算法。基于布尔函数运算的时序电路设计验证器我们提出了一种基于布尔函数运算的设计验证算法，该算法采用分支时间规则时序逻辑(BRTL)作为描述语言，与传统的时序逻辑相比具有更强的表达能力。开发了基于该算法的设计验证器，并成功地进行了微处理器的设计验证。有效的布尔函数操作我们已经阐明了共享二叉判定图(SBDD)操作布尔函数的理论性质。提出并实现了使图变小的输入变量排序算法和在二级存储上高效处理大数据量SBDD的算法。逻辑综合器和设计验证器的图形界面我们在工作站上利用X Window系统实现了一个多机多屏系统，实现了高分辨率和高速绘图。

项目成果

K.Hamaguchi: "Formal Verification of Speed-Dependent Asynchronous Circuits Using Symbolic Model Checking of Branching Time Regular Temporal Logic" Proceedings of the 3rd Workshop on Computer-Aided Verification. 2. 478-488 (1991)

K.Hamaguchi：“使用分支时间正则时序逻辑的符号模型检查对速度相关异步电路进行形式化验证”第三届计算机辅助验证研讨会论文集。

H.Higuchi: "Compaction of Test Sets Based on Symbolic Fault Simulation" Proceedings of the Synthesis and Simulation Meeting and International Intercharge. 253-262 (1992)

H.Higuchi：“基于符号故障仿真的测试集压缩”综合与仿真会议和国际交流会议论文集。

H. Hiraishi: "Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification" Proceedings on Computer-Aided Verification. 279-290 (1991)

H. Hiraishi：“用于顺序机器验证的计算树逻辑的矢量化符号模型检查”计算机辅助验证论文集。

K.HAMAGUCHI: "Formal Verification of Speed-Dependent Asynchronous Circnits Using Symbolic Model Checking of Branching Time Regular Temporal Logic" Proceedings of the Workshop on Computer-Aided Verification. 478-488 (1991)

K.HAMAGUCHI：“使用分支时间正则时序逻辑的符号模型检查对速度相关异步电路进行形式化验证”计算机辅助验证研讨会论文集。

H. Ochi: "A Vector Algorithm for Manipulating Boolean Functions Based on Shared Binary Decision Diagrams" Supercomputer 46. VIII. 101-118 (1991)

H. Ochi：“基于共享二元决策图操作布尔函数的矢量算法”超级计算机 46。