基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法

利用人工智能最新研究成果——约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较．首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解．该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束．实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高．

约束逻辑编程中宽数据算术运算算法

提出了一种在利用约束逻辑编程生成RTL数据通路模拟矢量的方法中处理宽数据的新方法。该方法解决了现有CLP求解器所能处理的最大整数限制问题。该文设计并实现了宽数据加法、减法和乘法运算的分解算法，运算分解扩展了现有CLP的功能，使其能适应实际的数据通路设计。实验结果表明方法是有效的。

基于CLP模型的HDL设计可观测性分析

为了提高模拟验证中的可观测性覆盖率,建立了一个逻辑约束编程(CLP)模型,定义了变量之间单步传播的条件.在此基础上,借助通用CLP系统自动地完成路径搜索、冲突发现、回溯和约束求解.实验结果表明,基于CLP的可观测性分析技术一方面可以生成更有效的测试向量,使得特定语句上的错误能够被传播到输出,加快模拟验证发现bug的过程;另一方面可以识别出不可观测的语句,避免盲目追求高覆盖率,节约模拟验证的资源.

文学经典的跨学科阐释——以《献给艾米丽的玫瑰》为例

从苏珊·桑塔格到哈罗德·布鲁姆,西方文学批评界反对阐释的声音时有所闻,但在西方文学批评史上,人们对于文学经典的阐释从未停止过。本文以美国作家威廉·福克纳发表于1930年的短篇小说《献给艾米丽的玫瑰》为例,结合20世纪90年代以来出现的3个具体的跨学科的阐释个案,考察这部小说在数学、认知科学和计算机科学等跨学科视角的审视下所展示出的阅读、理解与阐释可能性,思考立足跨学科的经验和知识结构解读和阐释一部文学经典给我们带来的启示。