公开(公告)号：CN1710567A

公开(公告)日：2005-12-21

申请号：CN200510027606.5

申请日：2005-07-07

Applicant: 复旦大学

Inventor： 丁敏 ,  唐璞山

IPC: G06F17/50

Abstract: 本发明属于超大规模集成电路技术领域，具体为一种时序电路等价验证的方法。本发明利用可满足问题算法作为引擎，以时间帧展开的验证算法为框架，结合了数学归纳法、不可满足子集提取和结构不动点等验证技术。步骤包括：生成初始结构不动点集合、对电路组合部分按时间帧展开、对结构不动点的验证等。其中，帧展开过程中采用了准动态约束生成算法，验证过程中采用了改进的可满足问题算法，大大提高了时序电路等价验证的效率。

公开(公告)号：CN1525550A

公开(公告)日：2004-09-01

申请号：CN03151031.0

申请日：2003-09-18

Applicant: 复旦大学

Inventor： 丁敏 ,  唐璞山

IPC: H01L21/82 ,  H01L21/66 ,  G06F17/50

Abstract: 本发明为一种解决超大规模集成电路验证的可满足性问题方法。它以深度优先搜索为基础，加入了推理过程，并利用推理过程对决策的策略做了相应的改进。具体步骤包括：决策过程、布尔约束的简化过程、回溯过程、学习过程和推理过程。其数据结构采用了2－3混合型变量监测数据结构形式。本发明方法可大大降低决策次数，提高工作效率。