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

利用状态缓存的时序等价性验证算法 被引量：1

Sequential Equivalence Checking Algorithm Using States Caching
下载PDF
导出
摘要 为了提高时序电路的等价性验证速度,提出一种改进的基于寄存器匹配的验证算法.除了利用原像计算避免误判之外,该算法还将可达状态和不可达状态引入到验证过程中.将仿真过程中从初始状态可以到达的状态记录为可达状态,将验证过程中确认不能从初始状态到达的状态记录为不可达状态,利用它们减少验证过程中的原像计算.基于mcnc91电路的实验数据表明,该算法有效地减少了验证时间. An improved algorithm based on register mapping is proposed to increase the speed of equivalence checking for sequential circuits. It not only used pre-image computation to avoid false negative, but also incorporated reachable states and unreachable states in the verification process. States that can be reached from the initial state in simulation are collected as reachable states, states that cannot be reached from the initial state in verification are collected as unreachable states, they are used to reduce pre-image computation. Experimental results based on mcncgl show that the algorithm can reduce verification time efficiently.
作者 杨军 翁延龄 葛海通 严晓浪
机构地区 浙江大学超大规模集成电路设计研究所
出处 《计算机辅助设计与图形学学报》 EI CSCD 北大核心 2008年第2期149-154,共6页 Journal of Computer-Aided Design & Computer Graphics
基金 国家自然科学基金(90207002)
关键词 时序等价性验证 寄存器匹配 原像计算 可达状态 不可达状态 sequential equivalence checking register mapping pre-image computation reachable states unreachable states
分类号 TP302 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献10

  • 1Mneimneh M N, Sakallah K A. Principles of sequentialequivalence verification [J]. IEEE Design & Test of Computers, 2005, 22(3): 248-257
  • 2Burch J R, Clarke E M, Long D E, et al. Symbolic model checking for sequential circuit verification [J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994, 13(4): 401-424
  • 3Touati H J, Savoj H, Lin B, et al. Implicit state enumeration of finite state machines using BDDs [ C ] //Proceedings of International Conference on Computer-Aided Design, Santa Clara, 1990:130-133
  • 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
  • 5Huang S Y, Cheng K T, Chen K C, et al. Aquila: an equivalence checking system for large sequential designs [J]. IEEE Transactions on Computers, 2000, 49(5): 443-464
  • 6Ranjan R K, Singhal V, Somenzi F, et al. Using combinational verification for sequential circuits [ C ] //Proceedings of the Conference on Design, Automation and Test in Europe, Munich, 1999:138-144
  • 7Anastasakis D, Damiano R, Ma H-K T, et al. A practical and efficient method for compare-point matching [ C] //Proceedings of Design Automation Conference, New Orleans, 2002. 305- 310
  • 8Lu F, lyer M K, Parthasarathy G, et al. An efficient sequential SAT solver with improved search strategies [ C] // Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, Munich, 2005:1102-1107
  • 9Yang S. Logic synthesis and optimization benchmarks user guide, Version 3.0 [R]. Research Triangle Park, North Carolina: Microelectronics Center of North Carolina, 1991
  • 10The SIS Group. SIS: a system for sequential circuit synthesis [R]. Berkeley: University of California, 1992

同被引文献12

  • 1Case 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.
  • 2Mishchenko 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.
  • 3van 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.
  • 4Ray 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.
  • 5Zhang 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.
  • 6Lu 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.
  • 7Mony 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.
  • 8Mishchenko A, Chatterjee S, Brayton R. FRAIGs: a unifying representation for logic synthesis and verification [R]. Berkeley: University of California, 2005.
  • 9Mony H, Baumgartner J, Paruthi V, et al. Exploiting suspected redundancy without proving it [C] //Proceedings of the 42rid Annual Design Automation Conference. New York: ACM Press, 2005:463-466.
  • 10郝亚男,杨海钢,谭宜涛,等.基于时序网络中冗余寄存器分类的冗余移除时序优化算法[C]//中国电子学会第23届电路系统分会会议论文集.桂林:桂林电子科技大学出版社,2011:126-13).

引证文献1

二级引证文献1

计算机辅助设计与图形学学报
2008年 第2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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