EDA技术日新月异,自顶向下硬件设计方法的应用日益广泛,不断显示出它的强大优越性。支持自顶向下设计方法的基本技术是自动综合,综合是EDA的关键技术之一。为了保证综合结果的正确,就必须对它进行验证。自动综合技术的发展给硬件设计正确性验证带来了新的问题。 数字系统高级综合包括数据通道综合和控制器综合。本文研究基于完全确定有限状态机模型的控制器综合的正确性验证,给出了基于图同构求解的验证方法。为了利用图同构方法对控制器综合进行验证,本文采用状态转换图STG_org表示控制器的源行为描述。状态转换图顶点中的多输入多输出逻辑函数表示对应状态的输出,图中边上的单输出逻辑函数表示状态转移条件;用一个八元组NetList表示控制器综合结果的结构实现,八元组包括输入符号,输出符号,状态存储器的输入,输出网络,状态转换网络,状态存储器,状态存储器的输出和状态存储器的初始输出。本文先从NetList逆向分析得到与控制器结构实现的行为等价的状态转换图STG_ext,然后分别对两个STG状态最小化,最后对两图利用图同构方法判定控制器综合前源行为描述与综合结果的行为描述是否等价。 在对控制器综合结果的正确性验证研究中,本文主要解决了下列两个问题: (1) 从控制器综合结果到控制器行为描述的逆向分析 (2) 两个完全确定有限状态机的状态转换图的同构证明 在解决上述问题过程中,设计了下列算法: (1) 逆向分析算法 (2) 两个完全确定有限状态机的状态转换图的同构算法 并对算法进行了较为详细的分析,给出了算法的时间复杂度。