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.