数字系统设计自动化中控制器综合的验证研究

论文摘要

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

论文目录

• 第一章 绪论
• 1.1 研究背景及选题意义
• 1.2 数字系统设计自动化概述
• 1.2.1 设计领域和层次
• 1.2.2 系统级综合
• 1.2.3 高级综合
• 1.2.4 RTL综合
• 1.2.5 逻辑级综合
• 1.2.6 工艺映射
• 1.3 控制器综合
• 1.3.1 有限状态机分解
• 1.3.2 状态化简
• 1.3.3 状态分配
• 1.4 测试
• 1.5 验证
• 1.6 本文完成的主要工作
• 1.7 小结
• 第二章 验证技术综述及控制器综合验证策略的确定
• 2.1 引言
• 2.2 验证方法概述
• 2.2.1 验证的基本概念
• 2.2.2 模拟验证
• 2.2.2.1 基本原理
• 2.2.2.2 步骤
• 2.2.2.3 方法
• 2.2.2.4 特点
• 2.2.3 符号模拟
• 2.2.4 形式验证
• 2.2.4.1 含义
• 2.2.4.2 任务
• 2.2.4.3 基本过程
• 2.2.4.4 目前的主要方法
• 2.3 符号模型检验
• 2.4 控制器综合验证策略的确定
• 2.4.1 适合控制器综合的验证方法的确定
• 2.4.2 基于STG图同构求解的控制器综合结果验证的基本思想
• 2.4.3 基于STG图同构求解的控制器综合结果验证方法的特点
• 2.5 小结
• 第三章 逆向分析技术的研究
• 3.1 引言
• 3.2 逻辑函数
• 3.3 控制器的行为描述
• 3.3.1 有限状态机
• 3.3.2 状态转换图
• 3.4 控制器的结构实现
• 3.5 逆向分析算法
• 3.5.1 基本思想
• 3.5.2 逆向分析算法
• 3.6 算法分析
• 3.6.1 算法推论
• 3.6.2 时间复杂性
• 3.7 小结
• 第四章 控制器综合结果的验证
• 4.1 引言
• 4.2 等价和最小化
• 4.2.1 状态等价
• 4.2.2 完全确定有限状态机的最小化
• 4.3 等价性验证
• 4.3.1 图同构问题的描述
• 4.3.1.1 图的同构
• 4.3.1.2 图同构求解的一般方法
• 4.3.2 等价性证明同构问题的描述
• 4.3.2.1 算法思想
• 4.3.2.2 等价性验证算法
• 4.4 算法正确性
• 4.5 算法复杂性讨论
• 4.6 小结
• 第五章 结束语
• 5.1 总结
• 5.2 将来的工作
• 参考文献
• 致谢