首页>
外国专利>
Lifting of bounded liveness counterexamples to concrete liveness counterexamples
Lifting of bounded liveness counterexamples to concrete liveness counterexamples
展开▼
机译:将有限的活动反例提升为具体的活动反例
展开▼
页面导航
摘要
著录项
相似文献
摘要
A trace of a bounded liveness failure of a system component is received, by one or more processors, along with fairness constraints and liveness assertion conditions. One or more processors generate randomized values for unassigned input values and register values, of the trace, and simulate traversal of each of a sequence of states of the trace. One or more processors determine whether traversing the sequence of states of the trace results in a repetition of a state, and responsive to determining that traversing the sequence of states of the trace does result in a repetition of a state, and the set of fairness constraints are asserted within the repetition of a state, and that the continuous liveness assertion conditions are maintained throughout the repetition of the state, a concrete counterexample of a liveness property of the system component is reported.
展开▼