集成电路的验证,已经成为其研发的最大障碍。传统的模拟验证技术无法满足当前SOC(System-On-Chip)设计带来的空前巨大的验证需求。基于此,形式化的验证方法作为模拟方法的一种重要补充,越来越得到人们的关注。模型判别技术(Model Checking)是形式验证技术的一种,用户参与少、自动化程度高,可以应用于电路设计的不同层次的优点使其成为该领域的研究热点。但是电路规模的增大,有限自动机的状态数以指数的形式增加,在实际中受到了有限内存的约束,这个问题就是模型判别中的瓶颈问题——状态空间爆炸。有限模型判别技术(BoundModel Checking,BMC)应运而生。传统的BMC技术基于BDD或SAT,而当前的设计主流是寄存器传输级(Register Transfer Level,RTL),其字位混合的约束使得传统的BMC技术极其低效。本文提出一种新颖的方法解决这个问题。首先将电路按照时序展开;接着使用线性规划(Linear Programming,LP)约束对RTL电路进行约束建模,生成隐式自动机;并将待验证的性质进行线性化描述,生成线性规划约束;最后是用LP求解器,得出验证结果。实验表明这种方法,较传统的BMC技术,在CPU时间和内存消耗上具有较大的优势。在进行上述技术研究时,我们发现如果能够将RTL设计的模块化层次式结构信息引入到验证系统中来,将对验证过程起到较大的指导意义。我们进一步开发了H-LPSAT系统。它可以验证层次式的RTL设计。实验表明H-LPSAT系统的验证效率,较上述方法有了更进一步的提高,尤其在CPU时间上。