定量约束的仿真跟踪验证
1. 引言
如今，嵌入式系统的复杂度不断增加，这就需要更先进的设计和测试方法。为了在市场上取得成功，产品需要集成更多的功能和特性，系统变得更加集成化。同时，由于在单个板卡模块或芯片上使用多种计算资源（如微处理器、数字信号处理器、可重构逻辑）在经济上变得可行，嵌入式系统架构也变得更加异构。
目前，嵌入式硬件和软件开发人员在寄存器传输级（RTL）或顺序C代码级进行设计已经不再高效。下一次生产力的大幅提升将来自系统级设计。功能和架构的规范应该在高层次抽象上进行定义，设计过程将包括细化抽象功能和架构，并通过自动工具或在工具支持下的手动方式将功能映射到架构上。与现有的固定架构和先验分区方法相比，高层次设计过程使设计师能够根据手头的功能定制架构，或修改功能以适应可用的架构，从而在设计灵活性、产品性能和成本方面带来显著优势。
为了将高层次系统规范的设计实践变为现实，从高层次抽象规范到低层次实现的设计流程中的每一步都需要验证方法的支持。系统级规范使得形式验证成为可能，设计师可以使用线性时态逻辑（LTL）、计算树逻辑（CTL）等逻辑来描述要检查的属性，并使用形式验证工具（如Spin模型检查器、Formal - Check、SMV）进行验证。然而，在低层次，复杂度可能会迅速超出自动工具的处理能力，此时仿真将成为验证的主要手段。
仿真的优势在于其简单性。尽管仿真的覆盖率受仿真向量数量的限制，但在实际设计中，它仍然是设计分析的标准工具。基于仿真的属性分析存在一个问题，即评估仿真跟踪并推断是否存在错误并不总是那么直接。本文提出了一种高效的自动方法，用于分析仿真跟踪并检查它们是否满足由指称逻辑公式指定的定量属性。待验证的属性用约束逻辑（LOC）编写，这是一种特别适
