利用状态缓存的时序等价性验证算法.pdfVIP

第20卷第2期 计算机辅助设计与图形学学报 Vd．20．No．2 2008年2月 oF GRAPHICS Feb．．2008 JOURNALCOMPUTER—AIDEDDESIGNCOMPUTER 利用状态缓存的时序等价性验证算法 杨 军 翁延龄 葛海通 严晓浪 (浙江大学超大规模集成电路设计研究所杭州310027) (yangiun@vlsi．zju．edu．en) 摘要 为了提高时序电路的等价性验证速度，提出一种改进的基于寄存器匹配的验证算法．除了利用原像计算避 免误判之外，该算法还将可达状态和不可达状态引入到验证过程中．将仿真过程中从初始状态可以到达的状态记录 为可达状态，将验证过程中确认不能从初始状态到达的状态记录为不可达状态，利用它们减少验证过程中的原像计 算．基于mcnc91电路的实验数据表明，该算法有效地减少了验证时间． 关键词时序等价性验证；寄存器匹配；原像计算；可达状态；不可达状态 中图法分类号TP302 States SequentialEquivalenceCheckingAlgorithmUsing Caching Jun Ge Yan Yang WengYanlingHaitongXiaolang (InstituteofVLSI 3 Design，ZhejiangUniversity，Hangzhou10027) AbstractAn basedon is toincreasethe of improvedalgorithm register speed mappingproposed for circuits．Itnot used toavoidfalse equivalencechecking sequential only pre—imagecomputation negative， butalso reachablestatesandunreachablestatesintheverification thatcan be incorporated process．States from as reachedtheinitialstateinsimulationarecollectedreachablestates，statesthatcannotbereached fromtheinitialstateinverificationarecollectedasunreachable areusedtoreduce states，they pre．image resultsbasedonmenc91 showthatthe canreduceverificationtime computation．Experimental algorithm efficiently． words sequentialequivalence computation；reachablestates； Key checking；registermapping；pre-image unreachablestat