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