数字系统的组成可分成数据通道部分和控制器部分，相应的自动综合便分成数据通道综合和控制器综合。控制器综合优化方法的研究涉及到许多理论问题，解决好这些理论问题，寻找到新的实用、有效的控制器综合优化算法是建立实用的EDA系统的关键之一。同时，控制器综合的正确性需要检验或证明，控制器综合结果的正确性证明处于相对薄弱的环节。 随着数字电路规模和设计优化程度的不断提高，控制器必须使用非完全确定有限状态机模型才能满足要求，完全确定有限状态机模型将显得越来越不够用。使用非完全确定有限状态机模型，其非完全性质和具有的随意性可显著提高自动综合的优化程度。其不仅提高了自动综合算法的复杂程度，而且更增大了形式验证的难度。本文采用形式验证方法，研究基于非完全确定有限状态机模型的控制器综合的正确性验证，给出基于状态转换图的相容性验证算法。 本文主要工作和贡献包括： 1．研究了状态化简和状态分配技术进展，介绍了非完全确定有限状态机的状态化简的方法，分析了经典的按权状态算法原理以及存在的问题。 2．从控制器综合结果逆向分析出等价的行为描述。 3．基于非完全确定有限状态机模型的控制器综合前行为描述STG_org与综合结果的行为描述STG_ext的相容性证明。具体包括： (1) 首先判断控制器综合过程中状态化简的正确性，即判断STG_org与进行状态最小化得到的STG_rd的相容性。利用了控制器综合的相关信息，有效的降低了算法的时间复杂度。 (2) 然后给出STG_rd与STG_ext的相容性验证算法。