在过去几十年,人们对信息技术大量需求,微电子技术高速发展,使得集成电路的规模和复杂度越来越高,这些对集成电路的设计和制造提出了更高的要求。在亿万级的晶体管电路中,完全不出现错误是非常难的,1994年Intel公司的芯片中的浮点错误就是一个例子,因此设计验证已经越来越受重视。STE是基于四值符号模拟的模型验证技术,在大规模硬件设计中发挥了很大的作用。尽管STE验证很高效,但是STE的固有缺陷是它验证的属性种类有限,对于无限时间属性无能为力,另外STE断言只能进行前向模拟,不进行后向模拟,所以也无需查找反例。在最近的一些年,GSTE(广义符号轨迹赋值,Generalized symbolic trajectory evaluation)是对STE扩展最成功的一个理论,GSTE可以验证无限时间性质,同时还可以进行后向模拟,由于GSTE具有可以后向模拟的特点,所以可以应用GSTE的这个特点进行本课题的研究,即研究GSTE理论的反例生成。因为GSTE一般进行的是性质相关的验证,性质一旦失败,就需要为其生成一个反例,提供给设计者来调试失败的错误,通过反例来确定失败的原因。设计者通过对于反例的调试,可以确定这个错误是由于无效的输入引起的,还是由于设计错误导致的。在前一种情况下,需要加入约束来消除无效性,后一种则需要系统设计返工。由于GSTE理论比较新颖,目前并没有学者对于GSTE的反例查找进行系统的研究,所以本课题进行反例查找技术的研究,对于GSTE理论的完善来说至关重要。本文首先对验证的发展进行了介绍,并重点介绍了STE验证理论和GSTE验证理论,并对它们的优缺点进行了分析。然后介绍了查找反例技术的发展,并重点介绍了其在GSTE理论中的的作用,基于以上原因,重点设计了两个查找反例的算法,通过这两个算法补充了GSTE理论在反例查找方面的欠缺。当应用GSTE进行验证时,如果出现断言错误时,可以使用第一个算法找出系统的一个反例。紧接着对第一个算法进行扩展,当出现断言错误时,可以使用扩展算法将与此错误相关的所有反例全部列出来。设计完算法后,本文通过编程实现了设计的算法。设计实现了编译模块、GSTE验证模块和反例查找模块。在算法的实现过程中,引入了Hash函数和BDD(二叉判定图,Binary Decision Diagram),通过Hash函数和BDD的运用,很大的提高了系统的效率,最后通过实例分析了系统的效率和可行性。