近年来，由于电路规模不断增大和电路功能日趋复杂，使得大规模集成电路的设计很难保证逻辑设计的正确无误。为了设计和建立高可靠性的VLSI系统，必须对VLSI的设计和实现进行有效的验证。目前主要的验证方法有模拟验证和形式验证两种，模拟验证是当前工业界使用的主要方法，但是由于单纯的模拟验证已不能满足VLSI设计和制造的需要，形式验证的方法越来越引起人们的重视。 模型检验(Model checking)方法是一种很有前途的形式验证方法，它的验证方法是通过对有限状态空间的遍历来确认规范说明(Specification)是否得到满足。这种方法具有高度自动化，执行速度快，能产生反例来帮助调试等特点，比较适合于VLSI的验证。 有效地建立和表示时序逻辑电路的状态转移关系是应用模型检查方法验证时序逻辑电路的关键技术之一。作者详尽地讨论了如何用二元判决图(BDD)表示时序逻辑电路的状态转移关系，在此基础之上，作者考察了一种单位时延的电位异步时序电路，提出并实现了表示其稳定状态转移关系的算法。 符号模型检验(Symbolic Model checking)是时序逻辑模型检验的技术一种具体方法，它使用一种更为有效的“符号”的方法来表示被检验系统，因而可以处理更大规模的系统。SMV系统是一种典型的符号模型验证系统，作者对SMV系统进行改进之后，初步实现了一个符号模型检验系统。该系统使用基于BDD的符号模型检查算法，可以比较有效地验证时序逻辑电路。