通用接口控制器GPIO_WB IP核设计与实现

通用IO接口是SoC系统中非常重要的一种外围端口。本文完成了一种基于WISHBONE总线的GPIO_WB控制器IP核的逻辑设计和物理实现，较具体地介绍了GPIO_WB IP核的体系结构以及WISHBONE接口和DMA传输方式的设计方案，并对所设计实现的GPIO_WB性能及可重用性做了分析，结论表明，与已有的通用IO接口IP核相比，GPIO_WB IP核具有性能高、实现代价小、硬件简单、可重用性好、易于扩展等优点。     

基于悖论分析和增量求解的快速反例压缩算法

使用反例压缩算法,从反例中剔除冗余信息,从而使反例易于理解,是目前的研究热点.然而,目前压缩率最高的BFL(brute force lifting)算法,其时间开销过大.为此,提出一种基于悖论分析和增量式SAT(boolean satisfiablilty problem)的快速反例压缩算法.首先,根据反证法和排中律原理,该算法对每一个自由变量v,构造一个SAT问题,以测试v是否能够避免反例.而后对其中不可满足的SAT问题,进行悖论分析,抽取出导致悖论的变量集合.所有不属于该集合的变量,均可作为无关变量直接剔除.同时,该算法使用增量式SAT求解方法,以避免反复搜索冗余状态空间.理论分析和实验结果表明,与BFL算法相比,该算法能够在不损失压缩率的前提下获得1～2个数量级的加速.     

基于否证蕴含的极小一阶不可满足子式求解算法

解释公式不可满足的原因在软件分析与验证等众多领域都具有非常重要的理论与应用价值,而极小不可满足子公式能够为公式不可满足的原因提供精炼的解释,帮助应用领域的自动化工具迅速定位错误,准确地诊断问题失败的本质缘由.文中针对极小一阶不可满足子式的求解问题,引入了否证蕴含图及其正向与逆向可达结点的概念,并证明了不可满足子式与否证蕴含图之间的关系.基于二者的关系,提出了基于冲突分析与否证蕴含的极小一阶不可满足子式求解算法,并融合了蕴含图剪枝技术,以提高算法效率.通过实验与当前最优的深度优先搜索算法进行了比较,结果表明:文中的算法显著优于深度优先搜索算法,并且随着公式复杂度的增加,性能优势更加明显.     

嵌入式微处理器的可测性设计技术研究

文章介绍了一个嵌入式微处理器的可测性设计技术。根据嵌入式微处理器各个组成部件逻辑功能的特点,分别采用了内置自测试(BIST)、部分扫描(PartialScan)、边界扫描(BoundaryScan)等方法完成各个部件的可测性设计,并将符合IEEE1149.1的TAP控制器作为整个微处理器的测试控制器,达到了较优的可测性设计结果。     

布尔不可满足子式的求解方法研究进展

解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值.不可满足子式能够为布尔公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由.针对近年来出现的许多求解布尔不可满足子式的研究工作,根据算法的类型归类比较,对各种求解方法进行了概述评论,并简要介绍了在该领域所做的一些研究工作.最后讨论了布尔不可满足子式的求解方法目前面临的主要挑战,并对今后的研究方向进行了展望.     

基于指令分解的微处理器验证与RTL级错误定位

本文提出并实现了一种新的基于指令分解的微处理器验证与RTL级错误定位方法。该方法从指令集模拟器的模拟结果中将指令分解为功能单元上的操作序列，并且输入和输出数据。将该结果与RTL模型的模拟结果比较，使RTL级错误定位精确到功能单元级。相对于传统的方法，大大提高了效率。     

一种求解布尔不可满足子式的局部搜索算法

解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而不可满足子式能够为公式不可满足的原因提供精确的解释,帮助应用领域的自动化工具迅速定位错误,诊断问题失败的本质缘由。近年来涌现了许多基于SAT求解器DPLL回溯搜索过程的完全算法,但关于不完全方法提取不可满足子式的研究相对较少。因此,本文提出一种采用启发式局部搜索过程从公式的不可满足性证明中求解布尔不可满足子式的算法。该算法根据公式的消解规则通过局部搜索过程直接构造证明不可满足性的消解序列,并融合了布尔推理技术以提高搜索效率;而后通过一个递归过程遍历证明序列从而得到不可满足子式。通过实验与贪心遗传算法进行对比,结果表明本文提出的算法优于贪心遗传算法。     

一种新型混合互连网络拓扑结构的分析与优化

随着高性能互连网络规模的增大,如何通过互连网络拓扑结构的设计来提升系统的性能和降低物理开销成为了系统设计的关键之一。传统的拓扑结构(可分为直接网络和间接网络)在网络规模增加时,不能很好地折衷网络性能和物理开销的关系。2012年Roberto P等人提出一种新型混合的拓扑结构,结合了直接网络和间接网络的特点,有效考虑了物理开销和网络性能的折衷。在此基础上,将新型混合拓扑每一维上的唯一的一个间接网络优化为多个间接网络,经过理论分析和实验模拟新型混合拓扑结构优化后的混合拓扑结构以及较常用的传统拓扑结构,优化后的混合拓扑结构能够在提升网络性能的同时降低物理开销。     

可满足性求解技术研究

求解公式的可满足性在诸如形式化验证、电子设计自动化与人工智能等众多领域中都具有非常重要的理论与应用价值,成为近年来的研究热点。本文针对命题公式与一阶公式的可满足性问题,重点介绍了布尔可满足性与可满足性模理论求解技术的基本原理,并且根据算法的类型进行分类阐述,分析了各种算法的优缺点。最后,讨论了目前面临的主要挑战,对今后的研究方向进行了展望。     

最小布尔不可满足子式的求解算法

 解释布尔公式不可满足的原因在众多领域都具有非常重要的理论与应用价值,而最小不可满足子公式能够为公式不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误,诊断问题失败的缘由.针对最小不可满足子式的求解问题,提出并证明了布尔公式最小不可满足性与极大可满足性之间的关系.基于二者的关系,提出了求解最小布尔不可满足子式的贪心遗传算法与蚁群算法,并且通过实验与当前最好的方法分支-限界算法进行了对比,结果表明:两种算法在运算效率以及单位时间内剔除的短句数上都显著优于分支-限界算法,而贪心遗传算法优于蚁群算法.