A Unified Approach to Testing and Verification of Designs Synthesized from High-Level Specifications

本研究为与设计验证和制造测试相关的测试问题开发了一个统一的框架。设计验证问题转化为基于寄存器传输级规范的扩展有限状态机(EFSM)中的可达性问题，设计验证测试对应于EFSM表示中跟踪路径的输入输出序列。它们是通过求解涉及数据寄存器、内部总线和主输入的线性和非线性约束得到的。基于线性约束的闭合形式解可以在多项式时间内求解的结果，探索了几种约束求解的搜索策略。制造测试是通过完全扩展部分指定的验证向量来获得的，以便在门级电路描述中实现最大的故障覆盖率。验证和测试序列可以通过反馈迭代求精。这项研究的贡献包括复杂电路的建模工具，约束求解问题的算法，以及故障覆盖的新措施。

This research develops a unified framework for the test problems related todesign verification and manufacturing tests. The design verificationproblem translates to the reachability problem in an extended finite statemachine (EFSM) derived from the register-transfer-level specification.Design-verification tests correspond to input-output sequences tracingpaths in the EFSM representation. They are derived by solving linear andnonlinear constraints involving data registers, internal buses, and primaryinputs. Several search strategies for constraint solving are being exploredbased on our result that closed form solutions to linear constraints can becomputed in polynomial time. Manufacturing tests are obtained by fullyexpanding partially specified verification vectors so as to achieve maximumcoverage of faults in the gate-level circuit description. The verificationand test sequences can be iteratively refined through feedback. Thecontributions of this research include modeling tools for complex circuits,algorithms for constraint- solving problem, and new measures of faultcoverage.