RTL电路的混合可满足性求解和模型检验

本课题的研究目的是：在寄存器传输级（RTL）电路上研究和实现一种可行、高效的模型检验(MC)方法。这种方法是通过对混合可满足性问题（HSAT）的求解和应用来实现的。.本课题主要包含两个方面的研究内容：.1．.混合可满足性求解器的研究。这是一个同时包含有字（word）和位（bit）变量的、具有多种约束形式的混合可满足性问题。我们将在基于ATPG和基于扩展DPLL两种途径上研究解决HSAT问题的有效方法。变量决策和约束传播是其中的核心技术。.2．.基于HSAT的RTL模型检验技术的研究。其研究内容涉及：时序展开、从验证性质到HSAT问题的转换、HSAT求解、以及如何提高验证的完备性等问题。归纳推理和无界模型检验(UMC)是提高验证完备性的主要技术。.以上的两方面研究内容紧密相联，是解决RTL模型检验问题的最关键技术。