期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

改进的基于属性不变量生成和数学归纳法的时序逻辑优化算法 被引量：1

An Improved Sequential Logic Optimization Algorithm Based on Invariant Generation and Induction
下载PDF
导出
摘要 为了在时序逻辑综合中使电路面积和关键路径延迟同时得到快速优化,提出一种改进的基于假设后验证的时序优化算法.在位并行随机模拟提取候选属性不变量之前,利用寄存器共享来降低初始候选不变量数目,以减少SAT程序的频繁调用;然后利用推测化简模型和改进的数学归纳法将基本条件和归纳步骤合并处理,有效地降低了电路规模和关键路径延迟,同时提高了算法运行速度.实验数据表明,文中算法使寄存器和节点规模平均下降41%和48%,关键路径延迟减小30%;与同类方法相比,该算法运行时间平均下降17%. To optimize the circuit area and critical path delay simultaneously and fast in sequential synthesis, this paper presents an improved sequential logic optimization algorithm based on an ＂assume-then-prove＂ principle. Prior to applying bit-wise parallel simulation to derive initial candidate invariants, the algorithm makes use of registers sharing to reduce the number of the initial candidate invariants, with which the number of times in calling the SAT procedure can be decreased. Then, it merges the processes of base case and induction steps to improve the induction utilizing speculative reduction model. Therefore it can effectively reduce both the area and critical path delay of the implementation circuits, and improve the computational speed. Experiment results show that the presented algorithm achieves an average reduction in number of the registers and the number of the logic nodes by 41% and 48% respectively, and the critical path delay can be reduced by 30% on average. In comparison with similar method, the average runtime of the new algorithm decreased ：7%.
作者 郝亚男 杨海钢 路宝珠 崔秀海 张茉莉
机构地区 中国科学院电子学研究所可编程芯片与系统研究室 中国科学院研究生院
出处 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2012年第9期1232-1240,共9页 Journal of Computer-Aided Design & Computer Graphics
基金 国家重点基础研究发展计划项目(2011CB933202) 国家自然科学基金(61106033)
关键词 时序优化 假设后验证 位并行随机模拟 寄存器共享 推测化简模型 sequential optimization assume-then-prove bit-wise random simulation registerssharing speculative reduction model
分类号 TP301 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献13

  • 1黄娟,杨海钢,李威,谭宜涛,崔秀海.可编程逻辑阵列减少毛刺的低功耗布线算法[J].计算机辅助设计与图形学学报,2010,22(10):1664-1670. 被引量：4
  • 2Case M L. On invariants to characterize the state space for sequential logic synthesis and formal verification [D]. Berkeley: University of California. Department of Electrical Engineering and Computer Science, 2009.
  • 3Mishchenko A, Case M, Brayton R, et al. Scalable and sealably-verifiahle sequential synthesis [C] //Proceedings of IEEE/ACM International Conference on Computer-Aided Design. Piscataway: IEEE Computer Society Press, 2008: 234-241.
  • 4van Eijk C A J. Sequential equivalence checking based on structural similarities [J].IEEE Transactions on Computer- Aided Design of Integrated Circuits and Systems, 2000, 19 (7) : 814-819.
  • 5Ray S, Mishchenko A, Brayton R. Incremental Sequential equivalence checking and subgraph isomorphism [C] // Proceedings of IEEE International Workshop on Logic Synthesis. Los Alamitos: IEEE Computer Society Press, 2009 : 37-42.
  • 6Zhang J S, Sinha S, Mishehenko A, et al. Simulation and satisfiability in logic synthesis [C]//Proceedings of IEEE International Workshop on Logic Synthesis. Los Alamitos: IEEE Computer Societv Press. 2005, 161-168.
  • 7Lu F, Cheng K T. Ichecker: an efficient checker for inductive invariants [C] //Proceedings of the llth Annual IEEE International High-Level Design Validation and Test Workshop. Los Alamitos: IEEE Computer Society Press, 2006:176-180.
  • 8Mony H, Baumgartner J, Mishchenko A, et al. Speculative reduction-based sealable redundancy identification [C] // Proceedings of Conference on Design, Automation and Test. Los Alamitos; IEEE Computer Society Press, 2009: 1674- 1679.
  • 9Mishchenko A, Chatterjee S, Brayton R. FRAIGs: a unifying representation for logic synthesis and verification [R]. Berkeley: University of California, 2005.
  • 10闫炜,吴尽昭,高新岩.基于符号模拟和变量划分的SAT算法[J].四川大学学报（工程科学版）,2008,40(3):121-125. 被引量：3

二级参考文献37

  • 1Tuan T, Kao S, Rahman A, et al. A 90nm low-power FPGA for battery-powered applications[C]//Proceedings of the 14th ACM/SIGDA International Symposium on Field Programmable Gate Arrays, Monterey, 2006:3-11.
  • 2Anderson J H, Najm F N. Switching activity analysis and pre-layout aetivity prediction for FPGAs [C] //Proeeedings of the International Workshop on System-Level Interconnect Prediction, Monterey, 2003:15-21.
  • 3Rose J, Gamal A E, Sangiovanni-Vincentelli A. Architecture of field-programmable gate arrays [J]. Proceedings of the IEEE, 1993, 81(7) : 1013-1029.
  • 4Monteiro J C, Oliveira A L. Finite state machine decomposition for low power [C] //Proceedings of the 35th Annual Conference on Design Automation, San Francisco, 1998:758-763.
  • 5Kim D, Choi K. Power-conscious high level synthesis using loop folding [C]//Proceedings of the 34th Annual Conference on Design Automation, Anaheim, 1997:441-445.
  • 6Kandemir M, Vijaykrishnan N, Irwin M J, et al. Influence of compiler optimizations on system power [J]. IEEE Transactions on Very Large Scale Integration Systems, 2001, 9(6) : 801-805.
  • 7Lamoureux J, Wilton S J E. On the interaction between power-aware FPGA CAD algorithms [C] //Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, San Jose, 2003:701-708.
  • 8Chen D M, Cong J, Li F, et al. Low-power technology mapping for FPGA architectures with dual supply voltages [C] //Proceedings of the 12th ACM/SIGDA International Symposium on Field Programmable Gate Arrays, Monterey, 2004:109-117.
  • 9Monteiro J, Devadas S, Ghosh A. Retiming sequential circuits for low power [C]//Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, Santa Clara, 1993: 398-402.
  • 10Wilton S J E, Ang S S, Luk W. The impact of pipelining on Energy per operation in field-programmable gate arrays [M] // Lecture Notes in Computer Seience. Heidelberg: Springer, 2004:719-728.

共引文献5

同被引文献6

引证文献1

二级引证文献2

计算机辅助设计与图形学学报
2012年 第9期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部