FPGA_ASIC-AHB片上系统总线的建模及验证.pdf

电子发烧友 电子技术论坛 AHB 片上系统总线的建模与验证 作者:张辉，董荣胜 来源:微计算机信息 摘 要：如何有效的对 SoC 设计进行验证已经成为缩短设计周期的关键问题。针 对这个问题，本文提出一种形式化建模与验证方法，对片上系统 AMBA 工业总 线规范的 AHB 总线协议进行形式化规格；建立了与 AHB 协议规格对应的有限 状态机和 SMV 模型，使用 CTL 描述了仲裁器的公平性、从单元活性、从单元的 交互操作性、互斥性和无饥饿属性；采用 SMV 模型检验器对 AHB 总线协议模 型的无饥饿属性进行了自动化验证。结果表明所提方法能够有效应用于 SoC 的 验证。 关键词：AHB ；有限状态机；计算树逻辑；符号模型检验 1 引言 随着设计规模的增大和设计复杂度的提高，片上系统(SoC)的验证问题已经成为 缩短设计周期的瓶颈。而 SoC 设计使用总线协议来完成 IP 核之间的数据传输， 因此，为了验证IP 之间的交互作用，必须对总线协议模型进行验证。完全利用 传统的模拟仿真技术对其进行验证变得越来越困难，形式化验证方法正逐渐成为 一种可供选择的实用方法而受到广泛关注[1-3]。目前，片上系统总线主要有 AMBA 总线、CoreConnect 总线和 Wishbone 总线，由于 AMBA[4-5]总线独立于 处理器与制造工艺技术，可重用性较高，更是受到工业界的青睐，已成为一种流 行的工业标准片上结构。AMBA 总线规范包括 AHB 、ASB 、APB 和 Test Methodology 等四部分。其中，AHB 是最重要的部分，对芯片上模块之间的 互连具有重要意义。因此，本文针对 AMBA 工业总线规范中的 AHB 总线，给 出一种形式化建模与验证方法，通过对AHB 总线协议进行形式化规格，建立了 电子发烧友 电子技术论坛 与协议规格对应的有限状态机模型和 SMV 模型；采用 CTL 描述系统的属性，并 使用符号模型检验器对其进行自动化验证。文中实例的验证结果表明了所提方法 在 SoC 验证中的有效性。 2 AHB 总线协议规格 AHB 主要用于高性能模块(如 CPU、DMA 和 DSP 等)之间的连接，作为 SoC 的 片上总线，具有以下特性： 单个时钟边沿操作；非三态的实现方式；支持流水 线操作；支持突发传输；支持分段传输等。AHB 系统由主模块、从模块和基础 结构等 3 部分组成，AHB 总线上的传输是由主模块发出信号，从模块响应，当 响应为可接受时,主模块占用总线,进行数据传输。基础结构由仲裁器、主从模块 多路选择器、从主模块多路选择器、译码器、虚拟模块所组成。若总线上存在多 个主模块，就需要仲裁器来决定如何控制各种主模块对总线的访问。总线译码器 根据传输数据的地址选择为主单元服务的从单元，一次操作只能有一个总线从单 元被选中。 为便于对 AHB 协议进行规格，先定义以下符号： HBUSREQ ： 主单元 M 向仲裁器A 申请接入总线。 HGRANT ：仲裁器允许主 单元的总线请求。 HTRANS ： 当前传输的状态。若传输没有发生，HTRANS=IDLE ； 若当前传输 是突发传输中的第一次传输，则 HTRANS = NSEQ ，否则HTRANS=SEQ 。 HREADY ： 从单元 s 通过声明 HREADY 信号延迟时钟周期。 SPLIT： 从单元通过 SPLIT 响应通知仲裁器自己不能对主单元服务。 RETRY ： 从单元通过 RETRY 响应通知主单元m 再次进行传输。 OKAY ： 从单元通过 OKAY 响应来声明其可以为主单元服务。 HSPLIT ： 当从单元 s 准备好为主单元 m 服务时，声称 HSPLITm 信号。 MASKm ： 当且仅当仲裁器相信主单元m 已经被分离(split) 且没有被恢复时， 电子发烧友 电子技术论坛 MASKm 数组为真。 Di ，Ai ：协议允许主单元对地址 Ai 、Ai+1…进行突发传输数据(Di、Di+1…) 。 数据 Di 和地址 Di+1 在同一个 时钟周期内。 基于上述符号，AHB 协议可形式化定义为： (1) M→A ：HBUSREQm ；{MASKm(1，0)} ； (2) A→M ：HGRANTm ；{RESPm，MASKm(1 ，0)} ； (3) M→S：Di ；{Ai}dec，{HGRANT}，{RESP(OKAY，SPLIT|RETRY)}； {HTRANS(IDLE，NSEQ ，SEQ)}； (4) S→M