基于EBES的异步电路逻辑符合验证

发布时间：2021-07-04 14:24

　　由于同步电路设计的局限性,如时钟偏移、抖动、噪声和能耗方面,异步电路设计越来越受到人们的关注。异步电路已被广泛应用于各类电子系统中,因此它们的正确性必须仔细考虑。对异步电路的行为的描述和验证,是关于异步电路系统研究的关键问题。近些年,大多数的模拟和验证使用的都是基于状态的形式化模型,而基于动作的形式化模型,即事件结构,因为建模过程复杂的原因,很少被应用于系统的形式化仿真模拟和验证。本文选择扩展的绑定事件结构（EBES）对异步电路进行建模和验证,并对EBES的进程代数语义进行详细的介绍。事件是事件结构的基本单元,事件表示一个动作的发生,那么如何在异步电路中获取动作是十分关键的。为此,在本文中给出了从信号传输波型中获取动作的方法。通过信号传输波形,将每个信号分为4个动作,其中包含两个稳定动作表示信号的有效传输。根据EBES的定义,文中呈现了简单逻辑门的标记语义。由于复杂逻辑可以由基本逻辑单元组合而成,因此可以以组合的形式构建其EBES。异步电路的验证主要是判断其EBES实现和规范是否具有一致性。在使用互模拟等价检验时发现,要达到预想的结果,必须给实现添加太多的限制,但这样的电路是很难设计出... 

【文章来源】：兰州大学甘肃省 211工程院校 985工程院校 教育部直属院校

【文章页数】：54 页

【学位级别】：硕士

【部分图文】：

进程代数的操作语义

图 3-1 如何在波型中获取动作图 3-1 中呈现的波形，可以通过信号波形的组合来描述一个仅仅描述信号的高低变化，而且描述了从高电平到低电平的变化趋势。通过动作可以自然而然地抽象出信号的变化中，可以抽象出 4 个动作。当信号的电压小于 low 可以得到压值高于 high 可以得到动作 as+；当信号的电压高于 low 并于上升时，可以得到动作 a+；但当处于下降状态时，相应在实际电路中，信号也不是在最高点才是有效的，它是达到出去，因此上述动作的提取方法是可以正确的描述一个信号述描述，任何信号均可被分为 4 个动作，例如信号 a 可以被+和 as-。辑门的 EBES

号 a 和信号 b 是无依赖关系的，以根据每个逻辑门的 EBES 图得基本逻辑门的 EBES 后，接下介绍如何从简单逻辑门的 EB实现包含许多原始的与/或逻辑单元起。形式上，连接的引脚包含几间的通信来执行组合行为就像真，如何确保所有的通信过程跟真。通过并行组合操作，我们可以

【参考文献】：
期刊论文
[1]基于高阶π演算的构件演化行为研究[J]. 何海洋,李强,余祥,韩翔宇.  计算机科学. 2017(03)
[2]基于硬件模拟的SAT求解框架[J]. 何安平,毛乐乐,谌知学,吴尽昭.  微电子学与计算机. 2016(09)
[3]基于Spin的安全协议形式化验证技术[J]. 冉俊轶,吴尽昭.  计算机应用. 2014(S2)

博士论文
[1]多项式代数事件结构及其近似和近似等价[D]. 王超.北京交通大学 2016
[2]扩展π演算的建模、验证与测试[D]. 罗玲.西安电子科技大学 2015
[3]基于动作细化的异步电路自动综合[D]. 孙秀莉.中国科学院研究生院（成都计算机应用研究所） 2005

硕士论文
[1]基于CSP的城轨CBTC联锁逻辑形式化建模与验证[D]. 马慧.北京交通大学 2013
[2]基于Petri网的异步电路设计研究[D]. 谢晔.江苏大学 2008
[3]基于SPIN的ATM交换机行为的验证[D]. 吴孝军.兰州大学 2006
[4]概率进程代数的度量指称语义[D]. 曾琼.中国科学院研究生院（成都计算机应用研究所） 2006



本文编号：3264956