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

摘要

数字系统高级综合包括数据通道综合和控制器综合。本文研究基于完全确定有限状态机模型的控制器综合的正确性验证，给出了基于图同构求解的验证方法。为了利用图同构方法对控制器综合进行验证，本文采用状态转换图STG_org表示控制器的源行为描述。状态转换图顶点中的多输入多输出逻辑函数表示对应状态的输出，图中边上的单输出逻辑函数表示状态转移条件；用一个八元组NetList表示控制器综合结果的结构实现，八元组包括输入符号，输出符号，状态存储器的输入，输出网络，状态转换网络，状态存储器，状态存储器的输出和状态存储器的初始输出。本文先从NetList逆向分析得到与控制器结构实现的行为等价的状态转换图STG_ext，然后分别对两个STG状态最小化，最后对两图利用图同构方法判定控制器综合前源行为描述与综合结果的行为描述是否等价。

目录

文摘

英文文摘

论文说明：图表目录

独创性声明和学位论文版权使用授权书

第一章绪论

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.3符号模拟

2.2.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.2等价性证明

4.4算法正确性

4.5算法复杂性讨论

4.6小结

第五章结束语

5.1总结

5.2将来的工作

参考文献

致谢