公理模型到操作模型的自动转换：理论与实践

系统可建模为操作模型（具有显式的状态及状态间转移概念）或公理模型（完全由一组不变量指定）。大多数形式化方法技术（如 IC3、不变量综合等）为操作模型设计，对公理模型基本不可用。此外，此前不存在将公理模型自动转换为操作模型的方法，因此公理模型的操作等价模型须手动创建并证明等价。本文推进了公理到操作模型转换的技术水平。我们表明，$\mu$spec 公理建模框架中的一般公理无法翻译为等价的有限状态操作模型。我们还推导了对 $\mu$spec 公理空间的限制，使其可行地生成等价的有限状态操作模型。在实践结果方面，我们开发了将 $\mu$spec 公理自动翻译为等价有限状态基于自动机的操作模型的方法论。我们通过使用我们过程生成的模型来证明三个 RTL 设计上序性质的正确性，展示了方法的有效性。