论文标题
同步数字逻辑系统的高级规范和验证的框架
A Framework for the High-Level Specification and Verification of Synchronous Digital Logic Systems
论文作者
论文摘要
提出了一个句法模型，用于规范具有复杂输入/输出接口的有限同步数字逻辑系统，该系统控制着不透明的计算元素之间的数据流，以及组成兼容系统以形成没有输入或输出的闭环系统。该模型以一种新颖的方法来改进类似的现有模型，以统一和对称的方式指定输入和输出端口。还提出了用于编码任意计算过程的自动机模型，并提出了算法以生成闭环系统的自动机表示。使用自动机模型，针对所需的行为规范对闭环系统的定时态度验证的问题，被编码为闭环系统在执行的一组计算方面的相似性，被证明是可决定的。讨论了模型与系统实现之间的关系。
A syntactic model is presented for the specification of finite-state synchronous digital logic systems with complex input/output interfaces, which control the flow of data between opaque computational elements, and for the composition of compatible systems to form closed-loop systems with no inputs or outputs. This model improves upon similar existing models with a novel approach to specifying input and output ports in a way which is uniform and symmetric. An automaton model is also presented for encoding arbitrary computational processes, and an algorithm is presented to generate an automaton representation of a closed-loop system. Using the automaton model, the problem of timing-agnostic verification of closed-loop systems against a desired behavioural specification, encoded as the similarity of closed-loop systems in terms of the set of computations performed, is shown to be decidable. The relationship between the models and real-world implementations of systems is discussed.
