Temporal Specification Verification

本研究是对同步和异步数字系统中模块互连的时序规范进行验证。时间行为的概念是从功能行为的概念中抽象出来的，主要关注模块的控制协议，而忽略了模块计算的数据值。在该模型中，给出了各个模块的接口协议以及模块之间的连通性。建立静态图，描述各模块所有外部信号之间的时间关系。验证过程是基于图所表示的系统的可能行为与一组约束所表示的合法行为之间的比较。关键约束是一个模块的时间行为不能违反系统中另一个模块的时间约束。这些算法支持多个系统状态、状态转换以及协议内条件和循环的检查。这种搜索很容易处理，因为不考虑模块生成的功能行为和数据值。

Levitan This research is on verifying timing specifications for interconnection of modules in both synchronous and asynchronous digital systems. The notion of temporal behavior is being abstracted from the notion of functional behavior by focusing primarily on the control protocols of the modules and ignoring the data values computed by the modules. In this model, the interface protocols of each module are given along with the connectivity between modules. A static graph is built that describes the temporal relationships among all the external signals of all the modules. The verification process is based on a comparison between the possible behaviors of the system, represented by the graph, and the legal behaviors as represented by a set of constraints. The key constraint is that the temporal behavior of one module cannot violate the temporal constraints of another module within the system. The algorithms support multiple system states, state transitions, and checking of conditionals and loops within the protocols. This searching is tractable because functional behavior and data values generated by modules are not considered.