位置：立项数据库 > 立项详情页
采用形式化引擎加速处理器仿真验证收敛的关键技术研究
  • 项目名称：采用形式化引擎加速处理器仿真验证收敛的关键技术研究
  • 项目类别：青年科学基金项目
  • 批准号：60603049
  • 申请代码：F020302
  • 项目来源：国家自然科学基金
  • 研究期限：2007-01-01-2009-12-31
  • 项目负责人：沈海华
  • 负责人职称：副研究员
  • 依托单位：中国科学院计算技术研究所
  • 批准年度：2006
中文摘要：

本项目针对当前仿真验证中存在的问题，提出以形式化引擎求解覆盖率轨迹反馈驱动仿真测试向量生成，加速验证收敛。项目通过对可快速提供覆盖率轨迹的形式化引擎关键技术、覆盖率轨迹实时驱动处理器仿真验证的关键技术、支持多指令集的验证技术、基于片上多核处理器的多级覆盖率反馈技术等关键技术的研究，优化处理器仿真验证过程，实现加速功能验证收敛的目的。与现有覆盖率驱动技术相比，形式化引擎可在很短时间内求取覆盖率轨迹，在速度和实现开销上具有优势。本项目的研究突破了现有覆盖率驱动的随机仿真验证和形式化技术与仿真相结合的半形式化验证技术框架，在理论上具有研究价值；同时，本项目的一系列研究成果已成功应用在国产处理器的验证实践中，显示了广泛的应用前景。

中文主题词： 形式化验证、覆盖率、仿真、微处理器验证
结论摘要：

英文主题词Formal verification; Coverage; Simulation; Microprocessor Verificaiton

成果综合统计
成果类型
数量
  • 期刊论文
  • 会议论文
  • 专利
  • 获奖
  • 著作
  • 35
  • 22
  • 9
  • 0
  • 0
期刊论文
龙芯 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设计可观测性分析
一种高性能北桥芯片的设计及性能分析
一种基于SAT的运算电路查错方法
一种向分支指令后插入冗余指令的容错微结构
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号原型系统北桥的设计与实现
会议论文
Low power techniques on a high speed floating-point adder design
CREA: A checkpoint based reliable micro-architecture for superscalar processors
Concerning with on-chip network features to improve cache coherence protocols for CMPs
An Effective Approach For Subtreshold And Gate Leakage Power Estimation Of SRAM
Designing an effective constraint solver in coverage directed test generation
Effective Debugging CMP Design in Acceleration/Emulation
On Detecting Regular Predicates in Distributed Systems
Fast complete memory consistency verification
An accurate analysis of microprocessor design verification
Instruction level test for parallel multipliers
A clock system for high speed and low power parallel link
Energy-Efficient Input Buffer Design using Data-Transition Oriented Model
An Efficient Instruction Level Functional Verification of Processor Core with JTAG
DMA Cache: Using On-Chip Storage to Architecturally Separate I/O Data from CPU Data for Improving I/
Testing content addressable memories using instructions and march-like algorithms
Fetching primary and redundant instructions in turn for a fault-tolerant embedded microprocessor
Coverage directed test generation: Godson experience
Formula-Oriented Compositional Minimization in Model Checking
Snooping and Ordering Ring--- An Efficient Cache Coherence Protocol for Ring Connected CMP
A General Method to Make Multi-Clock System Deterministic
A Multi-FPGA Based Platform for Emulating a 100M -transistor-scale Processor with High-speed Periphe
Optimizing Power and Throughput for M-Out-Of-N Encoded Asynchronous Circuits
专利
随机测试程序生成方法和系统以及设计验证方法
模型检测中的模型抽象方法及其系统
验证向量的优化方法及装置
一种自动纠错系统及方法
覆盖率驱动随机验证集成电路的方法及系统
一种微处理器验证中快速换页的装置和方法
一种用于指令级随机验证的指令组合过滤方法及系统
用于验证电路的模型检测中的模型抽象方法及其系统
微处理器浮点单元的随机验证方法及系统
沈海华的项目
全面验证片上多核处理器技术、工具及方法研究
期刊论文 30 会议论文 11 专利 6