论文部分内容阅读
形式验证存在状态爆炸的问题,特别是软硬件的协同验证难以解决.为此研究了片上系统的协同形式验证问题,给出了一种高效的协同形式验证环境Co-Formal,用于从行为级到具体实现级的软硬件协同形式验证.以一个实际的硬件系统验证了该环境的可用性.
协同形式验证环境Co-Formal的建立与应用
【摘 要】
：
形式验证存在状态爆炸的问题,特别是软硬件的协同验证难以解决.为此研究了片上系统的协同形式验证问题,给出了一种高效的协同形式验证环境Co-Formal,用于从行为级到具体实现
【机 构】
：
上海交通大学电子工程系,上海交通大学电子工程系上海200030,上海200030
【出 处】
：
上海交通大学学报
【发表日期】
：
2003年z1期
其他文献
给出了基于支持向量机(SVMs)和RBF神经网络的软测量建模方法.通过对这两种方法进行理论分析和仿真比较研究,结果表明,SVMs方法跟踪性能好、泛化能力强、对样本的依赖程度低,它比基于RBF神经网络的软测量建模具有更好的推广能力.
以油罐车为背景,研究平放柱箱液体晃动的模态响应.采用Galerkin方法建立了贮箱平动激励下离散的液体受迫晃动方程,建立了三维受迫晃动响应的等效力学模型.首先考核了晃动特征
提出了一种基于小波域上的自适应图像水印嵌入方法,它根据各小波子带的噪声敏感度和视觉掩盖特性,将基于Legendre序列的伪噪声水印添加到图像各小波子带的特定数据上.实验结
在流体为无粘不可压和流动有势的假定下，研究了轴对称体的定常局部空泡流。空泡层流采用压力恢复模型，应用高阶有限元离散的边界积分方程方法，求解给定空泡数下的解。探讨了空泡
分析了光寻址空间光调制器对加续图像采样和能量量化所产生的噪声和假频，判别出产生噪声主要高斯噪声，借助电子学中A／D转换前置滤波概念，提出了一种光学前置滤波的方法，即在傅立叶
膜生物反应器(MBR)在污水处理方面极具前景,在我国受到广泛地关注。然而膜污染严重影响膜通量,增加系统运行成本,制约MBR的进一步发展。本文从膜污染分类及其影响因素两方面,
以基于有限自动机的多模式匹配算法（DFSA）为基础，结合Boyer-Moore(BM）和Quick Search（QS)快速单模式匹配算法的优点，提出了一种快速的多模式字符串匹配算法，在一般情况下，该算法不需