Ground Temporal Logic: A Logic for Hardware Verification
Ground Temporal Logic: A Logic for Hardware Verification
复制标题
地面时态逻辑：硬件验证逻辑
DOI：
10.1007/3-540-58179-0_59
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
P. Narendran
中科院分区：
文献类型：
--
作者：
D. Cyrluk;P. Narendran
我们提出了一种新的时态逻辑GTL，它适合于在寄存器传送级描述硬件的属性。我们认为，对于一些自然的硬件验证问题，该逻辑代表了对模型检查的改进。我们证明了该逻辑的有效性问题是π11完全的。然后，我们确定可判定的逻辑片段。我们表明，在这个片段中，我们仍然能够编码许多有趣的问题，包括流水线微处理器的正确性。
We present a new temporal logic,GTL, appropriate for specifying properties of hardware at the register transfer level. We argue that this logic represents an improvement over model checking for some natural hardware verification problems. We show that the validity problem for this logic isπ11complete. We then identify a fragment of the logic that is decidable. We show that in this fragment we are still able to encode many interesting problems, including the correctness of pipelined microprocessors.