目前随着系统复杂度的增大和电子设计自动化技术的提高,验证过程在整个集成电路系统设计中所占的份量也越来越大,验证工作需要大量的人力资源和财力资源,并逐渐演变成设计工作的瓶颈,因为任何一种EDA工具都不能完全确保系统设计的正确性。随着半导体制造工艺水平的快速发展、以及系统规模的不断增大,使得传统的验证工具无法胜任目前系统设计正确性的验证任务。　　系统设计者常常面临着一系列巨大压力,设计不仅要达到较高的集成度,同时还要考虑面向市场的时间,所以系统设计者面临着功能完全准确和推向市场时间的双重压力。当前复杂的专用集成电路和IC芯片设计中的验证工作占用了整个设计过程的百分之七十甚至更多,验证工程师和设计工程师的比例约达到三比一才能确保系统设计顺利地进行。通常设计过程中的错误越早被发现,修改错误的代价将得到减低并且由错误带来的损失也将得到减小,所以对验证方法的研究势在必行。“最短的验证时间,最完备的验证结果”是目前系统设计正确性验证中的重点追求目标。　　综合就是由EDA设计工具自动完成系统设计的过程。数字系统常常包括数据处理器和控制器两大基本部件,相应地便有处理器综合和控制器综合,本论文主要研究控制器综合结果的正确性验证。所谓控制器综合技术是指经过一系列的优化和化简等手段,在实现预期功能的前提下,使得控制器芯片性能达到最优。论文采用有限状态机系统描述控制器综合前的规范行为,用电路网表表示控制器综合结果的结构实现。在较为深入、全面地研究控制器综合特点的基础上,采用状态转换图描STG_ORG与STG_EXT述控制器综合前后的行为功能,用三元组V=(Q,Y(X,Q),F(X,Q))表示图中的顶点,Q为状态标识,Y(X,Q)为控制输出函数,F(X,Q)为状态转换函数,论文采用多维体阵列表示Y和F,为了判断两多维体的等价性,论文引入了多维体同或运算符,采用基于同或运算符的永真式判定算法验证相应顶点对的等价性。　　论文用多维体逻辑函数描述状态转换图各个顶点的控制输出和状态转换条件,采用便于计算机内部表示的多维体阵列描述多维体逻辑函数;然后利用永真式判定算法判断当前顶点对的控制输出函数是否一致;若一致,再利用论文定义的多维体同或运算符求出当前顶点对的所有下一顶点对,递归地采用永真式判定算法匹配当前顶点对的所有下一顶点对。基于永真式判定算法的验证方法适于高抽象层次、高复杂度、高集成度系统设计的正确性验证。　　论文第五章给出一个简单饮料控制器的规范描述,然后在Quartus II环境下,用VHDL语言实现该饮料控制器,并对设计结果进行了模拟验证;任意给定两个状态转换图,首先最小化两状态转换图,然后给出图中顶点对应的三元组V=(Q,Y(X,Q),F(X,Q))描述,最后采用永真式判定算法递归匹配当前顶点对。本文采用永真式判定方法判断当前顶点对输出函数的一致性,采用多维体同或运算符求解当前顶点对的所有下一状态。　　文章提出的利用永真式方法判定两状态图是否等价的方法,适合于面向高抽象层次与高复杂度控制器综合结果的正确性验证。