基于完全确定有限状态机的控制器综合的验证

摘要：

控制器综合从较高的抽象层次开始，使用硬件描述语言，采用综合优化工具进行，因此验证综合过程的正确性至关重要。本文采用图同构的方法对控制器综合前的完全确定有限状态机STG_org和从综合后结构实现逆向提取的完全确定有限状态机STG_ext进行等价性证明，从而验证综合过程的正确性；为进一步降低算法时间复杂度，利用综合过程状态化简的信息，提出带综合信息指导的验证算法，将时间复杂度从O(B2/A·t1(n)+A·t2(m,n))降低到D(B·t1(n)+A·t2(m，n))，理论上证明了算法的高效性。

关键词： 完全确定有限状态机 控制器综合 形式验证 时间复杂度 状态转换图 硬件描述语言

作者: 李炜 刘政怡 吴建国

作者单位: 安徽大学计算机科学与技术学院,安徽合肥 230039;安徽大学计算智能与信号处理教育部重点实验室,安徽合肥 230039 安徽大学计算智能与信号处理教育部重点实验室,安徽合肥 230039;安徽大学软件学院,安徽合肥 230039

会议类型: 国内会议

会议名称: 全国第19届计算机技术与应用学术会议(CACIS·2008)

会议地点: 合肥

会议语种:中文

页码: 1075-1080

在线出版日期: 2008-07-15（万方平台首次上网日期，不代表论文的发表时间）