RTL电路的混合可满足性求解和模型检验
批准号：
60673034
项目类别：
面上项目
资助金额：
25.0 万元
负责人：
吴为民
依托单位：
学科分类：
计算机图形学与虚拟现实
结题年份：
2009
批准年份：
2006
项目状态：
已结题
项目参与者：
李大法、于浚泊、赵燕妮、邓澍军、张剑、杨晓庆、蒋晨茜、林栋、伍绍贺
项目摘要
结项摘要
项目成果
吴为民的其他基金
相似基金
相关文献
中文摘要
本课题的研究目的是：在寄存器传输级（RTL）电路上研究和实现一种可行、高效的模型检验(MC)方法。这种方法是通过对混合可满足性问题（HSAT）的求解和应用来实现的。.本课题主要包含两个方面的研究内容：.1．.混合可满足性求解器的研究。这是一个同时包含有字（word）和位（bit）变量的、具有多种约束形式的混合可满足性问题。我们将在基于ATPG和基于扩展DPLL两种途径上研究解决HSAT问题的有效方法。变量决策和约束传播是其中的核心技术。.2．.基于HSAT的RTL模型检验技术的研究。其研究内容涉及：时序展开、从验证性质到HSAT问题的转换、HSAT求解、以及如何提高验证的完备性等问题。归纳推理和无界模型检验(UMC)是提高验证完备性的主要技术。.以上的两方面研究内容紧密相联，是解决RTL模型检验问题的最关键技术。
英文摘要
期刊论文列表
专著列表
科研奖励列表
会议论文列表
专利列表
登录
查看更多内容
Uncertainty relation
不确定性关系
不确定性关系
DOI：
--
发表时间：
--
期刊：
Physical Review A
影响因子：
2.9
作者：
[Dafa Li]
通讯作者：
Dafa Li
Bounded Model Checking Combining Symbolic Trajectory Evaluation Abstraction with Hybrid Three-Valued SAT Solving
结合符号轨迹评估抽象与混合三值 SAT 求解的有界模型检查
结合符号轨迹评估抽象与混合三值 SAT 求解的有界模型检查
DOI：
10.1007/978-3-540-72863-4_31
发表时间：
2006-05
期刊：
Lecture Notes in Computer Science
影响因子：
--
作者：
[Jinian Bian, Shujun Deng, Weimin Wu]
通讯作者：
Weimin Wu
DOI：
--
发表时间：
--
期刊：
计算机辅助设计与图形学学报
影响因子：
--
作者：
[邓澍军, 吴为民, 边计年]
通讯作者：
边计年
An entanglement measure for n qubits
n 个量子位的纠缠度量
n 个量子位的纠缠度量
DOI：
10.1063/1.3050298
发表时间：
2007-10
期刊：
Journal of Mathematical Physics
影响因子：
1.3
作者：
[Dafa Li]
通讯作者：
Dafa Li
Classification of four-qubit states by means of a stochastic operation and the classical communication invariant and semi-invariant
通过随机操作和经典通信不变式和半不变式对四量子位状态进行分类
通过随机操作和经典通信不变式和半不变式对四量子位状态进行分类
DOI：
--
发表时间：
--
期刊：
影响因子：
--
作者：
[]
通讯作者：
共 10 条
面向RT级电路的分级模型判别技术
-
批准号：60273011
-
项目类别：面上项目
-
资助金额：20.0万元
-
批准年份：2002
-
负责人：吴为民
-
依托单位：
国内基金
海外基金