用FPGA的快速进位器优化卫语句的硬件综合

文章在给出类OCCAM语言卫语句文法与语义的基础上,探讨了当前将其综合为FPGA网表的方法,分析了这种方法的不足。结合FPGA芯片的特性,文章提出了一种基于进位多路器的综合优化方法。试验验证了该方法的有效性,它不但减少了资源开销,同时提高了芯片的运行速度。

模型检验中对CTL公式的空属性探测

在模型检验中建立了一种新方法:检验可计算时态逻辑(CTL)公式描述的系统属性是否为空属性.根据原子命题的极性,用TRUE或FALSE替换原子命题,得到一系列的CTL公式,再对这些CTL公式用模型检验工具验证,若CTL公式中有一个通过了验证,则可得出该系统属性是一个空属性.该方法对CTL公式的空属性的探测不需要对它的所有子公式用TRUE或FALSE替换,只需对原子命题替换,这样检验的次数与原子命题的个数呈线性关系.利用验证综合系统对十字路口交通控制器规范的空属性进行了检验.

基于有向图深度优先遍历的组合反馈环路检测算法

分析了造成数字逻辑设计在仿真过程中出现死循环的一个原因,提出了一种在仿真前发现设计中可能造成仿真时死循环的方法。方法主要分为三个步骤:1)分析数字逻辑设计中形成组合逻辑关系可能的文法形式。2)利用Juliano[1]三元组范式化方法对过程赋值语句进行范式化,从而判别哪些过程赋值是会生成组合逻辑电路。3)用有向图深度优先遍历方法发现组合反馈回路,以检测数字逻辑设计中组合回路的陷阱。并分析了算法复杂性。

高可信IP核交付标准应用

随着数字系统的日益复杂,基于IP(Intellectual Property)的设计方法成为缩短开发周期的必然之选。因此,高可信IP核构建技术成为IP核交付及IP核复用成功的关键。主要研究高可信IP核的构建方法,首先阐述高可信IP核,以及高可信IP核应具有的特点;然后在国内外各大IP核标准的基础上,结合形式化规范技术,给出了一个可操作的高可信IP核文档交付方案。

一种将人造物边界从自然背景中分离的新方法

对象的边界是图象识别的主要依据 ,但若对象处于一定的自然背景中 ,则自然背景的边界会给识别过程增加计算的负担 ,因此在识别前有必要将对象与背景的边界区别开 .该问题通常是通过基于“试探性阈值的方法”来解决 ,由于该方法未考虑边界点的局部特性 ,故该方法不能保留对象的细节 .为了解决这一问题 ,提出了一种将人造物边界从自然背景中分离出来的基于分形几何的新算法 .该算法基于对边界点的梯度强度阈值与曲线分形维数的考虑 ,用聚类分析的方法对边界点进行筛选 ,并利用以云 ,树丛为背景的飞机图象为实验对象 ,来验证该算法的有效性与优越性 .在这些例子中 ,可以看到大量自然背景的边界被滤掉了 ,而飞机的局部细节得到了保留 .最后又进一步探讨了该算法的适用范围 .

一种基于约束求解的Verilog语言静态分析方法

由于硬件描述语言Verilog中存在赋值语句的并发行为,对其验证一直是静态分析技术的一大挑战。针对Verilog程序的正确性问题,提出一种基于布尔约束求解的Verilog验证方法。通过分析Verilog语义特点,采用分步编码的方式对Verilog并发赋值语句进行处理。实验结果显示,该方法能有效地检测Verilog程序中设计的缺陷,并给出错误发生时程序的状态。

基于Mealy机精化关系的验证算法

与传统验证方法相比,形式验证技术因其完备性,已在数字电路设计领域中得到越来越多的关注。通过对形式验证技术和状态机的研究,在LTL公式的可实现策略基础上,提出一个基于Mealy机精化关系的验证算法,实现了一个搜索工具原型:支持算术表达式的LTL性质描述,在设计空间中搜索满足给定规范的输入输出信号。该技术可应用于定位电路设计中满足给定功能性质的代码片段。