位置：成果数据库 > 期刊 > 期刊详情页
一种基于SAT的运算电路查错方法
  • ISSN号：0254-4164
  • 期刊名称：计算机学报
  • 时间：0
  • 页码：112-115
  • 语言：中文
  • 分类：TP301[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
  • 作者机构：[1]中国科学院计算技术研究所计算机系统结构重点实验室,北京100080, [2]中国科学院软件研究所计算机科学国家重点实验室,北京100080
  • 相关基金：本课题得到国家“九七三”重点基础研究发展规划项目基金（2005CB321600）、国家“八六三”高技术研究发展计划项目基金（2002AA110010,2005AA119020,2005AA110010）、中国科学院知识创新工程重大项目基金“高性能通用CPU芯片研制”（KGCX1-SW-09）和国家自然科学基金（60603049,60673044）资助.致谢感谢审稿专家的建议.他们细致的工作对本文裨益良多.严俊和刘生也提出了宝贵的建议,在此一并致谢!
  • 相关项目：采用形式化引擎加速处理器仿真验证收敛的关键技术研究
作者： 陈云霁|沈海华|胡伟武|张健|
关键词： 形式验证, 模型检验, SAT, E—CNF, 标志子句, Formal verification, SAT, E-CNF, Tag clause
中文摘要：

基于SAT的运算电路查错方法将被验证系统中系统规范成立与否的问题转换为布尔公式和数学公式的混合形式E-CNF，通过采用了标志子句技术的E-SAT求解器进行求解．实验表明该方法自动化程度高，能处理大规模的运算电路，有较强的查找错误能力．

英文摘要：

E-CNF is hybrid of Boolean formula and mathematic formula. SAT-based arithmetic circuit bug-hunting method translates the verification problem into E-CNF, and solves E-CNF through E-SAT solver. E-SAT solver is an extension of complete SAT solver, with tag clause technique. Experiments show that SAT-based arithmetic bug-hunting method is powerful in finding bugs in arithmetic circuits.

同期刊论文项目
　延长摩尔定律的微处理芯片新原理、新结构与新方法研究
期刊论文 87
采用形式化引擎加速处理器仿真验证收敛的关键技术研究
期刊论文 35 会议论文 22 专利 9
经典逻辑和描述逻辑中的可满足性问题
期刊论文 8 会议论文 10
同项目期刊论文
组合测试：原理与方法
语义网的一阶逻辑推理技术支持
龙芯 2 号原型系统北桥的设计与实现
片上多核处理器存储一致性验证
基于支持向量机和功能覆盖率的验证向量优化
10 Gb/s receiver with half rate period calibration CDR and CTLE/DFE combiner
龙芯3A处理器封装的散热设计
基于龙芯2F处理器的硬件验证平台的设计与实现
Testing content addressable memories with physical fault models
覆盖率驱动的随机测试生成技术综述
基于遗传算法的全芯片级覆盖率驱动随机验证技术
基于长生命周期对象的混合垃圾收集
基于交易级建模的ATA控制器功能验证方法研究
IP可重用的AMBA AXI总线验证平台设计与实现
0.18 μm transmitter and receiver with high speed and low power
基于插桩分析的Java虚拟机自适应预取优化框架
片上多处理器中延迟和容量权衡的Cache结构
Chip Multithreaded Consistency Model
基于CLP模型的HDL设计可观测性分析
一种高性能北桥芯片的设计及性能分析
一种向分支指令后插入冗余指令的容错微结构
A 10 Gb/s receiver with half rate period calibration CDR and CTLE/DFE combiner
Making Effective Decisions in Computer Architects＇ Real-World： Lessons and Experiences with Godson-2 Processor Designs
基于覆盖率模型的AMBA接口随机验证方法
一个0．18μm高速低功耗的发送和接收电路
使用支持向量机的微处理器验证向量优化方法
通过增强数据访问局部性提高多路复用FIR滤波器计算性能
多核处理器片上网络trace压缩方法
龙芯2号原型系统北桥的设计与实现
龙芯2号处理器的同时多线程设计
龙芯3号互联系统的设计与实现
众核结构上分块LU分解算法的研究
New Methodologies for Parallel Architecture
通用处理器的高带宽访存流水线研究
一种片上众核结构共享Cache动态隐式隔离机制研究
众核处理器中使用写掩码实现混合写回/写穿透策略
众核体系结构对Cilk语言的硬件支持及评测研究
LU分解在众核结构仿真器上的指令级调度研究
Godson-T众核体系结构上的Broadcast性能优化
场景前颜色缓冲区压缩
带类型恢复的编译器源源翻译技术
片上多核处理器存储一致性验证
Godson-T: An Efficient Many-Core Architecture for Parallel Program Executions
高速低功耗传输电路的时钟系统设计
硬件结构支持的基于同步的高速缓存一致性协议
基于物理反标的处理器功耗建模与评估方法
Testing content addressable memories with physical fault models
基于遗传算法的全芯片级覆盖率驱动随机验证技术
片上实时功耗监控与估测的分析设计
一种基于元操作的宏模块功耗建模方法
一种模块级的温度感知漏电功耗估计策略
GALS处理器的功耗有效性方法研究
Physical Implementation of the 1GHz Godson-3 Quad-Core Microprocessor
基于长生命周期对象的混合垃圾收集
具有可变数据格式的透明度压缩
基于插桩分析的Java虚拟机自适应预取优化框架
一个基于微处理器功能模型的可靠度评估系统
片上多处理器中延迟和容量权衡的Cache结构
嵌入式处理器TLB设计方法研究
同时多微线程体系结构研究
跨平台系统级虚拟机的访存优化
一种基于RAM的降低异构多核切换开销的方法
龙芯3A多核处理器系统级性能优化与分析
基于硬件cache锁机制的Java虚拟机即时编译器优化
众核处理器片上同步机制和评估方法研究
二进制翻译控制转移的软硬件协同设计
嵌入式处理器在片调试功能的验证
结合访存失效队列状态的预取策略
龙芯2号微处理器的功能验证
一种高性能北桥芯片的设计及性能分析
一种向分支指令后插入冗余指令的容错微结构
A 10 Gb/s receiver with half rate period calibration CDR and CTLE/DFE combiner
浮点乘加部件的自动化形式验证
利用新型的电源屏蔽实现方法降低测试功耗
采用同步分析的零延迟GRLS通信机制
龙芯3号多核处理器的低功耗测试技术
片上偏差模型下Mesh结构时钟网络性能不确定性的分析
基于向量扩展多核处理器的矩阵乘法算法优化研究
Design and analysis of a UWB low-noise amplifier in the 0.18 μm CMOS process
混合体系结构中有状态硬件加速器的优化
LU分解在Godson—Tv1众核体系结构上的并行化研究
一个用于高速信号传输的对PVT变化不敏感的低功耗锁相环
高性能代价比的两层关联间接转移预测器设计
基于软硬件的协同支持在众核上对1-DFFT算法的优化研究
蛋白质序列比对算法在众核结构上的并行优化
龙芯处理器上的TLB性能优化技术
基于程序周期行为的快速模拟方法
Storus：一个二维片上网络拓扑结构
针对龙芯2号结构特征的GCC优化
基于SimpleScalar的龙芯CPU模拟器Sim—Godson
嵌入式处理器中访存部件的低功耗设计研究
龙芯2E北桥的设计和性能优化
基于覆盖率模型的AMBA接口随机验证方法
一种基于容量复用的异构CMP Cache
一种基于龙芯CPU的结构级功耗评估新方法
龙芯1号处理器的故障注入方法与软错误敏感性分析
龙芯2号微处理器浮点除法功能部件的形式验证
Xmesh：一个mesh—like片上网络拓扑结构
一种静态电路兼容的4GHz64位动态加法器设计
High Performance General-Purpose Microprocessors： Past and Future
一种快速的滑动标记缩并垃圾收集算法
Implementing a 1GHz Four-Issue Out-of-Order Execution Microprocessor in a Standard Cell ASIC Methodology
基于龙芯CPU的多核全系统模拟器SimOS—Goodson
使用支持向量机的微处理器验证向量优化方法
一种基于微基准程序和理想上限的处理器性能分析方法
一种分片式多核处理器的用户级模拟器
通过增强数据访问局部性提高多路复用FIR滤波器计算性能
多核处理器片上网络trace压缩方法
龙芯2号原型系统北桥的设计与实现
高性能通用处理器中的漏电功耗优化
龙芯1号处理器结构级功耗评估有效性分析
JTAG调试通信接口的软件模拟
Parallel Error Detection for Leading Zero Anticipation
通用处理器设计中硬件仿真验证
The Godson Processors： Its Research, Development, and Contributions
期刊信息
  • 《计算机学报》
  • 北大核心期刊（2011版）
  • 主管单位:中国科学院
  • 主办单位:中国计算机学会 中国科学院计算技术研究所
  • 主编：孙凝晖
  • 地址：北京中关村科学院南路6号
  • 邮编：100190
  • 邮箱：cjc@ict.ac.cn
  • 电话：010-62620695
  • 国际标准刊号：ISSN：0254-4164
  • 国内统一刊号：ISSN：11-1826/TP
  • 邮发代号:2-833
  • 获奖情况:
  • 中国期刊方阵“双效”期刊
  • 国内外数据库收录:
  • 美国数学评论（网络版）,荷兰文摘与引文数据库,美国工程索引,美国剑桥科学文摘,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊（2004版）,中国北大核心期刊（2008版）,中国北大核心期刊（2011版）,中国北大核心期刊（2014版）,中国北大核心期刊（2000版）
  • 被引量:48433