D0I:10.13374/j.issn1001-053x.2002.04.020 第24卷第4期 北京科技大学学报 Vol.24 No.4 2002年8月 Journal of University of Science and Technology Beijing Aug.2002 VLIW体系结构微处理器功能验证模型 王沁 北京科技大学信息工程学院，北京100083 摘要为了系统而有效地设计微处理器功能验证激励，针对VLIW体系结构微处理器的结 构特征，特别是多操作流水线并行特征，提出了VLW体系结构微处理器的功能验证模型，基 于该模型，针对一个规模为1500kbit等效逻辑门的VLW体系结构微处理器，完成了功能验证 方案的制定和10周期功能验证激励的设计 关键字VLIW;微处理器：功能验证；模型 分类号TP368.1 现代体系结构微处理器的一个共同的特征 2个方面定义一个VLIW体系结构微处理器. 是处理器内部操作并行性.这个特征使得“每条 1.1指令界面定义 指令功能正确，则处理器功能正确”的法则不再 VLIW指令格式的一般化表现形式为： 成立，从而增加了微处理器功能验证的复杂性 Format Flow_ctrl Opl Op2Op3 Op4 Op5Op6 因而，当具有现代体系结构特征的微处理器（如： 假设VLIW指令字中最多排列6个操作段， 多发射RISC体系结构微处理器，VLIW类体系 即Opi,i=l,…,6.Format为指令格式控制域，定 结构微处理器等)设计完毕后，设计功能正确性 义Flow_crl,Opi在指令字中的位置，以及Opi对 的验证比较复杂 应的部件.Flow ctrl为操作流控制域，定义Op 微处理器功能验证问题的关键在于定义能 的执行方式，包括条件执行、重复执行、并行执 够充分反映设计功能正确性的激励集合.目前， 行、和串行执行等.Opi为操作段，在确定Format 微处理器功能验证问题的研究成果主要在单发 编码下为对应于一个硬件单元（如：运算器单元、 射RISC体系结构微处理器的验证方面-，而对 寄存器、BUS等)的操作代码. 多发射RISC或VLIW体系结构微处理器功能 12组成定义 验证问题的研究结果还很少.从VLW体系结 VLIW体系结构微处理器组成定义为：M= 构微处理器的组成出发，提出了VLIW体系结 (U,E,I,INT). 构微处理器功能验证模型，作为定义功能验证 (1)能够独立工作的运算或存贮单元集合U. 激励集合的基础.本文首先定义了被验证对象 每个运算和存贮单元由操作数、操作码、流 一VLIW体系结构微处理器，在此基础上给出 水级数与输出结果之间的关系表示.即： 了VLIW体系微处理器的功能验证模型和功能 U={uyl,…,ym=u(op,xl,…,xn,t}. 验证激励设计流程. 例如，yl,y2)<=fau(opfau,.xl,x2,4),表示浮 点加减单元，xl,x2为操作数，opfau为浮点加减 1VLIW体系结构微处理器定义 单元的操作码，4表示浮点加减运算单元的流 VLIW类微处理器的指令格式和内部组成 水级数为4，y1为运算结果，y2为正常/异常状 各有不同.为论述方便，根据VLIW类微处理 态 器的本质性特征，从微处理器指令界面和组成 又如，(yl,…ym=reg(opn,xl,yl,…ym,l), 表示寄存器堆单元，x1为操作数，等式右端y1, 收稿日期2001-05-14王沁女，40岁，教授，博士 …ym表示寄存器堆在操作前的状态，等式左端 *863基金资助项目No.863-306-01-07) yl,",ym表示寄存器堆在操作后的状态，opn为 ★教育部优秀青年教师基金资助项目 写寄存器操作对应的寄存器编号，1表示寄存·
第 卷 第 期 年 月 北 京 科 技 大 学 学 报 珑触 加 几 】 呵 ， 体 系结构微处理器功能验证模型 王 沁 北京科技大学信息工程学院 ， 北京 摘 要 为 了系统而有效地设计微处理器功能验证激励 ， 针对 体系结构微处理器 的结 构特征 ， 特别是多操作流水线并行特征 ， 提出了 体系结构微处理器的功能验证模型 ， 基 于该模型 ， 针对一个规模为 等效逻辑 门的 体系结构微处理器 ， 完成 了功能验证 方案 的制定和 ， 周期功能验证激励 的设计 关健字 微处理器 功能验证 模型 分类号 现代体系结构微处理器的一个共同的特征 是处理器 内部操作并行性 这个特征使得 “ 每条 指令功能正确 ， 则处理器功能正确 ” 的法则不再 成立 ， 从而增加 了微处理器功能验证的复杂性 因而 ， 当具有现代体系结构特征的微处理器 如 多发射 体系结构微处理器 ，讥‘ 类体系 结构微处理器等 设计完毕后 ， 设计功 能正确性 的验证 比较复杂 微处理器功能验证 问题 的关键在 于定义能 够充分反 映设计功能正确性的激励集合 目前 ， 微处理器功能验证问题的研究成果主要在单发 射 体系结构微处理器 的验证方面 ‘ ， 而对 多发射 或 体系结构微处理器功能 验证 问题的研究结果还很少 从 体系结 构微处理器 的组成 出发 ， 提 出了 体系结 构微处 理器功能验证模型 ， 作为定义 功能验证 激励集合 的基础 本文首先定义 了被验证对象 — 体系结构微处理器 ， 在此基础上给出 了 体系微处理器 的功能验证模型 和功能 验证激励设计流程 体系结构微处理器定义 类微处理器 的指令格式和 内部组成 各有 不 同 ‘词 为论述方便 ， 根据 类微处理 器 的本质性特征 ， 从微处理器指令界面和 组成 收稿 日期 刁 一 王 沁 女 ， 岁 ， 教授 ， 博士 基金资助项 目 一 一 一 教育部优秀青年教师基金资助项 目 个方面定义一个 体系结构微处理器 指令界面定义 指令格式 的一般化表现形式为 卜 … 饰笋 伽 假设 指令字 中最多排列 个操作段 ， 即 ， ， … ， 为指令格式控制域 ， 定 义 ， 在指令字 中的位置 ， 以及 对 应 的部件 为操作流 控制域 ， 定义 ’ 的执行方式 ， 包括条件执行 、 重 复执行 、 并行执 行 、 和 串行执行等 吻 为操作段 ， 在确定 编码下为对应于一个硬件单元 如 运算器单元 、 寄存器 、 等 的操作代码 组成定义 体系结构微处理器组成定义为 二 ， ， ， 以 能够独立工作的运算或存贮单元集合 每个运算和存贮单元 由操作数 、 操作码 、 流 水级数与输 出结果之间 的关系表示 即 二 ，… ， ， ，… ， ， 例如 ， ， ， ， ， ， 表示 浮 点加减单元 ， ， 为操作数 ， 为浮点加减 单元 的操作码 ， 表示 浮点加减运算单元 的流 水级数为 ， 为运 算结果 ， 为正 常 异 常状 态 又如 ， ，… ， 令 叩 ， ， ，… ， ， ， 表示 寄存器堆单元 ， 为操作数 ， 等式 右端 ， … ， 卿表示 寄存器堆在操作前 的状态 ， 等式左端 ，… ， 表示 寄存器堆在操作后 的状态 ， 叩 为 写寄存器操作对应 的寄存器编号 ， 表示 寄存 DOI ：10．13374／j ．issn1001—053x．2002．04．020
Vol.24 No.4 王沁等：VLIW体系结构微处理器功能验证模型 ·459· 器操作的流水级数为1. 寄存器，pc∈(PC,PC+I),ul,u2,…,uk表示在int发 再如：假设不考虑存贮体系中的cache状态 生时正在执行的单元集合，i∈U. 和页表状态，则存取数单元的组成模型为y1,y2, y3,m,tlb)<=mem(1s,y1,y2,y3,m,tlb,2),其中，y1为 2功能验证模型 存/取数地址寄存器，y2为取数结果/存数数据 根据VLIW体系结构微处理器的指令界面 寄存器，y3为数据存取操作相关的状态标识寄 和组成定义，提出VLIW体系结构微处理器的 存器，m为存贮器，tb表示页表的快表，等式左 功能验证模型，用于支持功能验证激励的系统 右分别表示取数/存数操作前后的状态，1$为取 化的设计 数/存数操作符，2表示取数/存数操作的流水级 2.1U验证模型 数为2.类似地，可以得到考虑到cache和页表 因为U={u(yl,…,ym)K=u(op,xl,…,xn,t)}, 状态的存数/取数单元的组成模型 所以，对于U的一个完备验证模型是： (2)U上的通路集合E. OPxX1×.…xXn 每个通路由作为数据来源的运算或存贮单 其中，Xi是x的取值集合，然而，对于大多数单 元、选通控制信号等与作为数据使用者的运算 元而言，不可能完全遵循上述验证模型设计验 或存贮单元之间的关系表示.即： 证激励，因此，本文采用了等价类划分的方法确 E={m|k<=m(s,u0,….k-1),s=0,…,k 定各种单元的验证模型，即：针对不同操作的特 -l,ui∈U. 征将Xi,(i=1,,n)划分为若干等价类Xi1,…, 例如，u4=m(s,u0,u1,2,u3)表示存在一个 Xim),每个等价类中选择一个数据xjGj=l,…, 通路m,输入联接u0,ul,2,u3,输出联接u4,u4 m),构成Xi的关键数据集合Xi_key,于是验证 输入数据始终等于rs对应的ui的输出数据. 模型便成为： (3)指令格式集合I OPxX1_keyx…xXn_key 指令格式中的Format和Flow_ctrli域定义了 对于浮点数运算单元，将操作数先按照输 各个运算单元/存贮单元/通路等的操作码段在 入数据划分成等价类，得到等价类集合S0;再 VLIW字中可以出现的位置、以及执行方式（包 对S0中的各个数据集合按照输出数据特征划 括：无条件执行，有条件执行，并行执行，串行执 分等价类，得到等价类集合S1；然后针对操作 行，重复执行等).对于操作码段在VLW字的 码集合OP中的每一个操作opi,(i=l,…,m),对 位置，组成模型定义为： S1中的各个数据集合按照所经过的路径划分 I={<u_m,pos>u_mEUl E,pos in <len 0>, 等价类，得到等价类集合S21,S22,…,S2m;最 len为指令最高位} 后，从S2i的每一个等价类数据集合中拿出一 至于指令格式中定义的各个控制编码的执 个数据，从而构成操作i关键数据集合Xky 行方式，从功能验证的角度看，实质上定义了控 1.由此，两操作数的浮点运算单元验证模型为： 制编码是否有效和控制编码的有效时期.假设 (X key_1xX key 1)+(X key 2xX key 2)+...+ 控制编码的执行方式集合为EF,则上式扩展为 (X key_m x X key m) 如下形式： 参考文献[]是该验证模型在设计浮点单元 I={<u m,pos,effect>u_meU or E,pos in <len 验证激励中的具体应用 0>,len为指令最高位；effecte∈EF} 对于寄存器单元，根据CMOS寄存器单元 (4)中断规则集合NT. 特性，需要01翻转遍历每一位，所以可以将全 中断规则集合定义了被中断操作集合在特 1、全0、{10}序列、{01}序列构成一个X的关键 定机器状态下与中断返回地址和中断处理时机 数据结合Xkey,即有寄存器单元的验证模型 器状态之间的关系.即： 为： NT={int{(rl,…rm,sto,…,stm,pcK=int(ul,u2,…, OP X key. k,st0,…,stn)} 对于存贮器单元，由yl,y2,y3,m,tb)=mem 其中，st0,…,stm为中断相关的状态位，r1,…,m (s,y1,y2,y3,m,tb,2)可见验证模型必须考虑覆 为进入中断程序人口时各个流水线的外部可见 盖tb的各种情况及其组合，以及对于y3所对
、 】 ， 王 沁 等 体系结构微处 理器功能验证模型 器操作 的流水级数为 再如 假设不考虑存贮体系 中的 状态 和 页表状态 ， 则存取数单元的组成模型 为 工 ， ， ， ， “ ， ， ， ， ， ， ， 其 中 ， 为 存 取数地址 寄存器 ， 为取数结果 存数数据 寄存器 ， 为数据存取操作相关的状态标识寄 存器 ， 为存贮器 ， 表示 页 表的快表 ， 等式左 右分别表示 取数 存数操作前后 的状态 ， 为取 数 存数操作符 ， 表示取数 存数操作的流水级 数为 类似地 ， 可 以得到考虑到 和 页 表 状态 的存数 取数单元 的组 成模 型 上 的通路集合 每个通路 由作为数据来源 的运算或存贮单 元 、 选通控制信号等与作为数据使用 者 的运算 或存贮单元之间 的关系表示 即 二 二 ， ，· …泳一 声 二 ，、 二 ， 一 ， 任 ， 例如 ， ， ， ，， 表示 存在一个 通路 ， 输人联接 ， ， ， ， 输 出联接 ， 输入数据始终等于 对应 的 的输 出数据 指令格式集合 指令格式 中 的 和 域定 义 了 各个运 算单元 存贮单元 通路等 的操作码段在 字 中可 以 出现 的位置 、 以及执行方式 包 括 无条件执行 ， 有条件执行 ， 并行执行 ， 串行执 行 ， 重复执行等 对于操作码段在 字 的 位置 ， 组成模型 定义为 二 勺 ， 任 ， ， 为指令最高位 至 于指令格式中定义 的各个控制编码 的执 行方式 ， 从功能验证的角度看 ， 实质上定义 了控 制编码 是否 有效和 控制编码 的有效时期 假设 控制编码 的执行方式集合为 ， 则上 式扩展 为 如下 形式 “ 二娜 ， ， 一 任 ， 即 ， 为指令最高位 任 中断规则集合 则 中断规则集合定义 了被 中断操作集合在特 定机器状态下 与 中断返 回地址 和 中断处理时机 器状态 之间 的关系 即 二 ，… ， ，… ， ， 二 ， ， … ， ， ，… ， 其中 ， ， … ， 为中断相 关的状态位 ， ， … ， 为进人 中断程序人 口 时各个流水线 的外部可 见 寄存器 ， 任 ， ， ， ，… ， 表示在 发 生 时正 在执行 的单元集 合 ， 任 功能验证模型 根 据 体系 结构微处理 器的指令界面 和组 成定义 ， 提出 体系结构微处理器 的 功能验证模型 ， 用于 支持功能验证激励 的系统 化 的设计 验证模型 因为 ， … ， 卿 “ ， ，… ， ， ， 所 以 ， 对于 的一个完备验证模型 是 … 其 中 ， 是 的取值集合 然而 ， 对于 大多数单 元而 言 ， 不 可 能完全遵循上 述验证模型 设计验 证激励 ， 因此 ， 本文采用 了等价类划分的方法确 定各种单元 的验证模型 ， 即 针对不 同操作的特 征将 ， ， … ， 划 分为若干 等价类 ， … ， ， 每个等价类 中选 择一个数据 臼 ，… ， ， 构成 的关键数据集合 ， 于 是验证 模型便成为 少 … 少 对于 浮 点数运 算单元 ， 将操作数先按照输 入数据划 分成等价类 ， 得 到 等价类集合 再 对 中的各个数据集合按照输 出数据特征划 分等价类 ， 得 到等价类集合 然后针对操作 码集合 中的每一 个操作 叩 ， 只 ，… ， ， 对 中的各个数据集 合按 照所 经过 的路径 划分 等价类 ， 得到等价类集合 ， ， … … ， 最 后 ， 从 的每一 个等价类数据集合 中拿 出一 个数据 ， 从而构成操作 关键数 据集 合 少 ， 由此 ， 两操作数的浮 点运 算单元验证模型 为 一 一 夕 少 夕 二 沈 参考文献 是该验证模型在设计浮点单元 验证激励 中的具体应用 对 于 寄存器单元 ， 根 据 寄存器单元 特性 ， 需 要 翻转遍 历每一位 ， 所 以可 以将全 、 全 、 序列 、 序列 构 成 一个 的关键 数据结合 尼 ， 即有寄存器单元 的 验证模型 为 · 对于存贮器单元 ， 由 ， ， ， ， 二 ， ， ， ， ， ， 可 见 验证模型 必须考虑覆 盖 的各种 情况及其组合 ， 以及对 于 所对
。460· 北京科技大学学报 2002年第4期 应的各个输出状态的遍历.假设t山b有n个表项， yl…ym)←u(op,ml(rsl,ul0,,uln),m2 则根据快表的功能可将其状态等价划分为 (rs2,u20,….u2n),t). TLB_key={1个表项有效，2个表项有效，…， ulj,2j分别为第一、第二操作数来源单元. n个表项有效}，地址寄存器y1的状态可等价划 若不考虑走线延时带来的问题，则验证模型可 分为： 以定义为： ADR key=验证tb表的关键点数据集合+ OP×RS1×RS2, 验证存取操作正常/异常的关键数据集合. 其中，OP为操作编码集合，RS1,RS2分别为两 其中，验证tb表的关键点数据集合为{k个 个操作数的数据来源控制编码的集合，但是，为 表项有效时命中，k个表项有效时不命中，(k=1, 了保证运算操作第一级流水结果的正确性，则 ·,)},验证存取操作正常/异常的关键数据集 必须考虑从任何一个单元u可来的数据经过OP 合通过y3对地址集合进行等价划分得到. 上的任何一个操作的最长和最短路径后所得结 对于存数操作而言结果/数据来源寄存器 果的正确性.假设，通过OP上操作的最长和最 y2的状态可等价划分为Rkey={全0，全1，{10} 短路径的数据分别为a long,a short,则运算单 序列、{01}序列}，对于取数操作而言存贮器m 元上通路的验证模型应为： 的状态也可等价划分为Mkey={全0，全1，{10} OP×(Rs1×{a long,a_short})×(RS2×{a long, 序列、{01}序列}，操作码可以划分成存数操作 a short 集合ST和取数操作集合LD,于是得到存贮器 若数据通路的目标节点是寄存器堆单元， 单元的验证模型为： 则综合寄存器堆模型和联接寄存器堆的通路模 LD XTLB key×ADR key xM key+ST× 型得到： TLB key xADR key xR_key. (y1,.,ym)<=reg(opn,m(rs,u0,...,un),y1,.,ym,1) 因为构成微处理器的基本成分是组合电路 若不考虑走线延时带来的问题，数证模型 和时序电路，微处理器中任何单元都可以用运 可以直接定义为数据来源编码集合RS,即验证 算单元、或存贮单元、或2者的复合形式表示， 每个通路源节点到寄存器堆的通路是否正确. 所以，采用类似方法可以得到微处理器中所有 但是，由于寄存器堆中各个寄存器的物理位置 运算/存贮单元的验证模型， 不同，导致从每个数据源节点到其中每个寄存 2.2E验证模型 器之间的走线距离不同，所以，寄存器单元上通 E为U上的通路集合，即：E={m|k<-m 路的验证模型应为：OPN×RS (rs,u0,…,k-1),s=0,…,k-1,ui∈U}.在深亚微 OPN为寄存器堆中每个寄存器的写操作编 米工艺下实现VLW微处理器芯片，不仅通路 码集合. 之间的联接关系影响通路的功能正确性，而且 同理，可以推出联接存贮器单元及其它单 通路上两点之间的相对位置，即走线长度，也将 元的通路的验证模型 直接影响芯片功能的正确性.因为走线长度会 2.3I验证模型 影响通路的延时时间，而当延时时间超过设计 指令格式集合是VLIW体系结构微处理器 范围时将会导致最终结果不正确.为此，本文采 特有的集合.在一个超长指令字中，允许一个操 用了点到点之间通路遍历的验证模型，而不是 作代码段，包括运算或存贮单元代码段、或通路 通常采用的线遍历的验证模型.例如：通路m(rs, 控制代码段，出现在多个位置，并以不同方式执 u0,u1,u2,u3)的输出线L既是uj的输入，也是k 行.I验证模型的目的在于验证各个代码段的各 的输人，按照线遍历模型，只需要遍历1次s的 种出现及其组合的正确性， 4个取值，而按照点到点遍历模型，则需要遍历 假设，对于任意一个单元或通路的代码段 2次rs的4个取值，从而验证u0,ul,u2,3与ui, 记作code_i,它在指令上有效位置的集合为 u两两点之间联接的正确性和延时关系的正确 POSi,POSi的元素个数为n,则code i的指令 性. 格式验证模型为： 若数据通路的目的节点为运算单元，以两 {(pos ii,effect)pos ii∈POSi;effect∈EF}+ 操作数的运算单元为例，即有： ((pos ii,pos ij)pos ii,pos ijEPOSi++
北 京 科 技 大 学 学 报 年 第 期 应 的各个输 出状态 的遍历 假设 有 个表项 ， 则 根 据 快 表 的 功 能 可 将 其 状 态 等 价 划 分 为 个表项有效 ， 个表项有效 ， … … ， 个表项有效 ， 地址寄存器 的状态可等价划 分为 少 验证 表 的关键点数据集合 验证存 取操作正 常 异常的关键数据集合 其 中 ， 验证 表 的关键点数据集合为 个 表项 有 效 时命 中 ， 个表项 有效时不命 中 ， ， … ， ， 验证存取操作正 常 异 常 的关键数据集 合通 过 对地址集合进行 等价划分得到 对 于 存数操作而 言结果 数据 来源 寄存器 的状态可等价划分为 少 全 ， 全 ， 序列 、 序列 ， 对于取数操作而 言存贮器 的状态也可 等价划分为 抓全 ， 全 ， 序列 、 序列 ， 操作码可 以划分成存数操作 集合 和 取数操作集合 ， 于 是得 到存贮器 单元 的验证模型 为 少 少 ‘ ‘ ‘ · 因为构成微处理器 的基本成分是组合 电路 和 时序 电路 ， 微处理器 中任何单元都可 以用运 算单元 、 或存贮单元 、 或 者 的复合形式表示 ， 所 以 ， 采用 类似方法可 以得 到微处理器 中所有 运 算 存贮单元 的验证模型 验证模型 为 上 的通路集合 ， 即 二 ， ，… ， 一 ， ，… ， 一 ， 任 在 深亚 微 米工艺 下 实现 微处 理器芯 片 ， 不 仅通 路 之 间 的联 接关系影 响通路 的功能正 确性 ， 而且 通路上 两点之间的相对位置 ， 即走线长度 ， 也将 直接影 响芯 片功 能的正确性 因为走 线长度会 影 响通 路的延 时 时间 ， 而 当延 时时 间超过设计 范 围时将会导致最终结果不 正确 为此 ， 本文采 用 了点到点 之间通路遍历 的验证模型 ， 而不 是 通 常采用 的线遍历 的验证模型 例如 通路 ， ， ， ， 的输 出线 既 是 的输人 ， 也 是 的输人 ， 按 照 线遍历模型 ， 只需要遍历 次 的 个取值 ， 而按照 点到点遍历模型 ， 则 需要遍历 次 的 个取值 ， 从而验证 ， ， ， 与 ， 两两点之 间联接 的正确性 和延 时关系 的正 确 性 若数据通 路的 目的节 点为运 算单元 ， 以 两 操作数 的运 算单元为例 ， 即有 … ， ， ， … ， ， ， ， · … ， ， 分别为第一 、 第二操作数来 源单元 若不考虑走线延 时带来 的问题 ， 则验证模型 可 以定义 为 ， 其 中 ， 为操作编码集合 ， ， 分别为两 个操作数的数据来源控制编码的集合 但是 ， 为 了保证运算操作第一级流水结果 的正 确性 ， 则 必须考虑从任何一个单元 来 的数据经过 上 的任何一个操作 的最长 和最短路径后所得结 果 的正确性 假设 ， 通 过 上操作 的最长 和 最 短路径 的数据分别为 ， ， 则运 算单 元上 通路 的验证模型 应 为 ， 一 习 ， 一 若数据通 路 的 目标节 点是 寄存器堆单元 ， 则综合寄存器堆模型 和联接寄存器堆 的通路模 型 得 到 ，… ， ， ， ，… ， ， ，… ， ， 若不 考虑走线延 时带来 的 问题 ， 验 证模 型 可 以 直接定义 为数据来源 编码 集合 ， 即验证 每个通路源 节 点到寄存器堆 的通 路是否 正 确 但是 ， 由于 寄存器堆 中各个寄存器 的物理位置 不 同 ， 导致从每个数据源节点到其 中每个寄存 器之间的走线距离不 同 ， 所 以 ， 寄存器单元上通 路的验证模型 应 为 ‘ 为寄存器堆 中每个寄存器的写操作编 码 集合 同理 ， 可 以 推 出联接存贮器单元及其它单 元 的通路 的验证模型 验证模型 指令格式集合是 体系结构微处 理器 特有的集合 在一个超长指令字 中 ， 允许一个操 作代码段 ， 包括运算或存贮单元代码段 、 或通路 控制代码段 ， 出现在多个位置 ， 并 以不 同方式执 行 验证模型 的 目的在 于验证各个代码段 的各 种 出现及其组 合 的正 确性 假设 ， 对 于 任意一个单元或通路 的代码段 记 作 一 ， 它 在 指 令 上 有 效 位 置 的 集 合 为 一 ， 一的元素个数为 ， 则 的指令 格式 验证模型 为 印。 几 ， 任 ， 一 ， 任 一 …
Vol.24 No.4 王沁等：VLIW体系结构微处理器功能验证模型 ·461· {(pos_il,pos_i2,.,pos_in)I pos_il,pos_i2,, 的集合、和处理器中断相关状态s,中断将改变 pos_in∈POS_i}. 处理器中断相关的状态寄存器、各个正在工作 (posiⅱ，effect)表示code i在一个有效位置 的操作所在流水线的结果寄存器/结果寄存器 上出现，且以effect定义的执行方式执行.(pos 队列，并确定返回地址指针，因而验证微励设计 il,posi2,,pos_ik)表示code i在k个位置上出 的两个核心分别是处理器内流水线的工作状 现.对于所有的code i设计所述验证模型定义 态、中断相关的状态寄存器的取值.假设有n条 的验证激励，即可以完成对于VLW体系结构 流水线，p种中断，则由上节所述pipeline验证模 微处理器指令格式的验证. 型派生得到任意一种异常/中断的验证模型： 2.4 Pipeline验证模型 {U1 pipe+U2pipe++Un_pipe+(TIl×Tl2× Pipeline验证分为流水线自身验证和流水 …×T1m)+,…,t(Tk1×Tk2×…×Tkm)}×S0 线并行验证两个部分.流水线自身验证的目的 ×S1x…×Sp 在于验证一个流水线上流水操作之间的重叠. 其中，i1-im(行=1，…，k)流水线存在资源共享. VLIW体系结构微处理器的重要特点是显示指 Tj={(opij,t)|opj为u时j的任意一个有效操作； 令级并行处理，即指令之间的数据依赖关系由 t=0,1,…,t;0表示始终不启动操作，t=1,…, 优化编译器进行处理，从而保证了指令执行过 句表示该操作开始于第1，…，坷j周期}；Si为中断 程中不会因数据依赖关系造成流水线阻塞.这 响应时刻第i个中断相关的状态寄存器的有效 一特点降低了一条流水线本身功能验证的难 编码集合 度.假设uieU,且ui定义为yil,…,yim)K-ui(opi, 由验证模型可见，pipeline验证模型是中断 xil,…,xin,t,则其验证模型Ui pipe为： 验证模型的一个特例，因此可将2者有效结合， Ui pipe= 以减少实现相同验证能力的验证激励的数量. {t0,t1)川t0=1,t1=2,ti}+ 2个操作出现在流水线中 3功能验证流程 {t0,t1,t2)1t0=1,t2,t3=2,…ti且t2<t3}+ 微处理器验证模型已被成功地用于一个类 3个操作出现在流水现中 VLIW体系结构微处理器的验证工程中，功能 …+{(t0,t1,…,t)k=k)i级流水线充满 验证激励设计与仿真验证流程如下： 多个操作并行是VLIW体系结构微处理器 第1步，基于U验证模型设计运算或存贮单 的重要特征，这意味着可以有多个流水线并行， 元的功能验证激励集合.重点在于关键数据集 若流水线之间存在共享部件，则在验证流水线 合的选择和操作遍历.包括：(1)设计运算单元功 自身正确性后还需要验证流水线并行的正确 能验证激励集合；(2)设计通用寄存器单元功能 性.假设有ui,uj∈U,且ui,可j之间有资源共享，ui 验证激励集合；(3)设计存贮器单元功能验证激 定义为(yil,,yim)=ui(opi,xil,…,xin,ti),uj定 励集合；(4)设计特殊寄存器单元功能验证激励 义为(yj1,…yjmK=uj(opj,xj1,,xjn,),则ul,j 集合；（⑤）设计程序流控制单元功能验证激励集 2个流水线并行所对应的验证模型为： 合 Ti×Tj 第2步，基于E验证模型设计通路的功能验 其中，Ti={(opi,t)|opi为ui的任意一个有效操 证激励集合.重点在于遍历验证联接各个运算 作，t=0,1,…,i,(t=0表示始终不启动操作，=1， 或存贮单元的通路. ,ti表示该操作开始于第1，…，ti周期}.同理定 第3步，基于【验证模型设计指令格式的功 义j. 能验证激励集合，重点在于遍历验证运算单元 若处理器中允许有m个存在资源共享的流 操作码、存贮单元操作码、通路操作码等在 水线并行，则验证模型扩展为： VLIW指令字中各种可能的出现及其执行方式， T1×T2×.×Tm 第4步，利用pipeline验证模型设计验证各 2.5异常/中断验证模型 个流水线自身流水功能、流水线之间并行流水 由前面所述中断的组成模型可见，每一种 功能的正确性的验证激励.对于前者重点在于 中断都相关于中断发生时刻正在工作的单元u 遍历在一条流水线中允许出现的上下文关系；
王 沁 等 体系结构微处理器 功能验证模型 印 ， ， … ， ， 一 ， … ， 一 任 一 印 少 ， 表示 一在一个有效位置 上 出现 ， 且 以 定义 的执行方式执行 印 ， 心 ，… ， 表示 一在 个位置上 出 现 对于 所有 的 一设计所述验证模型 定义 的验证激励 ， 即可 以完成对于 体系结构 微处理器指 令格式 的验证 娜 验证模型 验证分为流水线 自身验证 和 流 水 线并行验证两个部分 流水线 自身验证 的 目的 在于 验证一个流水线 上 流水操作之间 的重 叠 体系结构微处理器 的重要 特点是显示 指 令级并行处理 ， 即指令之 间 的数据依赖关 系 由 优化编译器进行处理 ， 从而保证 了指 令执行过 程 中不 会 因数据依赖关系造成流水线 阻塞 这 一 特点 降低 了 一 条流 水 线 本 身功 能 验证 的难 度 假设 ，且 定义 为 ，… ， 二 ， ，… ， ， ， 则其验证模型 少 为 夕， ， ，… 个操作 出现在流水线 中 ， ， ， ， ，… ， 且 卜 刀 个操作 出现在流水 现 中 … ， ，… ， 级流 水 线充满 多个操作并行是 体系结构微处理器 的重要 特征 ， 这意 味着可 以有 多个流水线并行 ， 若流水线 之 间存在共享部件 ， 则在验证流 水线 自身正 确性 后 还 需要 验证 流水线 并行 的正 确 性 假设有 ， 任 ，且 ， 之 间有 资源 共享 ， 定义 为 ， … ， 叩 ， ， … ， ， ， 定 义 为 ，… ，刃 令 喇 ， ，一 ， ， ， 则 ， 个 流水线并行所对应 的验证模 型 为 其 中 ， ， 为 的任意 一 个有 效操 作 ， ， ，… ， ， 一 表示 始终不启动操作 ， 月 ， … ， 表示 该操作开 始 于第 ，， 二 ， 周期 同理定 义 若处理器 中允许有 个存在 资源共享 的流 水线并行 ， 则 验证模 型 扩展 为 米 … … 异常 中断验证模型 由前面所 述 中断 的组 成模型 可 见 ， 每一 种 中断都相 关于 中断发生 时刻正在工作 的单元 的集合 、 和处理器 中断相关状态 ， 中断将改变 处理器 中断相关 的状态寄存器 、 各个正在工 作 的操作所在 流水 线 的结 果 寄存器 结果 寄存 器 队列 ， 并确定返 回地址指针 因而验证激励设计 的 两 个 核心 分别是 处 理器 内流 水 线 的 工 作 状 态 、 中断相 关的状态寄存器 的取值 、 假设有 条 流水线 ， 种 中断 ， 则 由上 节 所述 验证模 型 派生 得 到 任意一种 异 常 中断 的验证模 型 夕 夕 … … ‘ ， … … ， ， 二 … … 其 中 ， 一 ，… ， 流 水线存在资源 共享 二 笼 ， 为 的任意一 个有效操作 一 ， ，… ， 卜 表示 始终不启动操作 ， 一 ，… ， 表示 该操作开始于 第 ，… ， 周 期 为 中断 响应 时刻第 个 中断相关 的状态 寄存器 的有效 编码集合 由验证模型 可 见 ， 验证模型 是 中断 验证模型 的一 个特例 ， 因此可 将 者有效结合 ， 以减少实现相 同验证能力 的验证激励 的数量 功能验证流程 微处理器验证模型 已被成 功地用 于 一 个类 体 系结构微处 理器 的验证工 程 中 功 能 验证激励设计与仿真验证流 程如 下 第 步 ，基于 验证模 型设计运 算或存贮单 元 的功 能验证激励集合 重 点在 于 关键数据集 合的选择和操作遍历 包括 设计运算单元功 能验证激励集合 设计通 用寄存器单元 功能 验证激励集合 设计存贮器单元功 能验证激 励集合 设计特殊寄存器单元功 能验证激励 集合 设计程序流控制单元功 能验证激励 集 鉴 第 步 ，基 于 验证模型 设计通 路的功能验 证激励集合 重 点在于遍 历 验证联接 各个运算 或存贮单元 的通 路 第 步 ， 基 于 验证模型 设计指 令格式 的功 能验证激励集 合 ， 重点在 于 遍 历 验证运 算单元 操作码 、 存 贮单 元 操 作码 、 通 路操 作码 等在 指令字 中各种 可 能的出现及其执行方式 第 步 ， 利 用 验证模型 设计验证各 个流水 线 自身流水功 能 、 流 水线 之 间并行 流水 功能 的正确性 的验证激励 对 于 前者重 点在 于 遍历 在 一 条 流水线 中允许 出现 的上 下 文 关系
·462· 北京科技大学学报 2002年第4期 对于后者重点在于遍历并行流水线所允许的各 体激励设计是十分重要的. 种上下文关系 第5步，在第4步产生的验证激励的基础 参考文献 上，利用异常/中断验证模型设计异常/中断功能 1 Li Shen,S Y H Su.A Functional Testing Method for 验证激励，重点在于验证各种并行流水执行过 Microprocessor [J].IEEE Trans on Computer,1988,37 (10):1288 程中和中断嵌套时中断机制的正确性. 2 El-sayed A Talkhan,Aly M H Ahmed,Aly E Salama. Microprocessor Functional Testing Technique[].IEEE 4结语 Trans on Computer Aided Design of Integrated Circuits and Systems,1989,8(3):316 随着微处理器规模的日趋增大、微处理器 3 Salama A E,Ali A K,Talkhan E A.Functional Testing of 组成的日趋复杂，微处理器功能验证问题也日 Pipelined Processor[J].IEE Proc Computer Digit Tech, 趋重要.本文提出的VLIW体系结构微处理器 1996,143(5):318 功能验证模型，其中采用了划分等价类、点到点 4 Laurent Fournier,Yaron Arbetman,Moshe Levinger.Func- 通路验证、流水线并行验证、流水线中断验证等 tional Verification Methodology for Microprocessors 思想和方法.基于该模型，针对一个规模为1500 Using the Genesys Test-Program Generator[C].[In:De sign,Automation and Test in Europe.Munich,Germany, K等效逻辑门的VLIW体系结构微处理器，完 1999.434 成了功能验证方案的制定，以及100000周期的 5曲英杰，夏宏，王沁.微处理器浮点运算功能的测试 功能验证激励的设计 方法研究[J.计算机工程与应用，2001,37(7)：42 在工程实践中发现研究功能验证模型，并 在功能验证模型指导下进行功能验证方案及具 VLIW Architecture Microprocessor Functional Verification Model WANG Qin Information Engineering School,UST Beijing,Beijing 100083,China ABSTRACT When the architecture and organization of microprocessor is becoming more and more com- plex,the problem about how to verify the microprocessor function is becoming more and more important.In order to design the functional verification stimulus of microprocessor effectively,a functional verification model of VLIW architectural processor is introduced,based on the organization characteristic,especially the parallel pipeline,in the VLIW microprocessor.Based on the verification model,a verification schema and 100,000 cycle of stimulus for a VLIW microprocessor design have been finished,which includes about 1500 Kbit gates. KEY WORDS VLIW;microprocessor;functional verification;model
一 北 京 科 技 对于后者重点在于遍历并行流水线所允许 的各 种上下 文关系 第 步 ， 在第 步产生 的验证激励 的基础 上 ， 利用 异 常 中断验证模型设计异常 中断功能 验证激励 ， 重点在于 验证各种并行流 水执行过 程 中和 中断嵌套时 中断机制 的正确性 大 学 学 报 体激励设计是十分重要 的 年 第 一 期 结语 随着微处理器规模 的 日趋增大 、 微处理器 组成 的 日趋复杂 ， 微处理器功能验证问题也 日 趋重 要 本文提 出的 体系结构微处理器 功能验证模型 ， 其 中采用 了划分等价类 、 点到点 通路验证 、 流水线并行验证 、 流水线 中断验证等 思想和方法 基于该模型 ， 针对一个规模为 等效逻 辑 门的 体系结构微处理器 ， 完 成 了功能验证方案 的制定 ， 以及 周期 的 功能验证激励 的设计 在工程实践 中发现研究功能验证模型 ， 并 在功能验证模型指导下进行功能验证方案及具 参 考 文 献 ， ’ ， 一 】 ， ， 介 ， ， ， 民 独上 ， ， 帅 ，、 恤 ， 。 、 乞 珑 一 肚 ， ， ， 曲英杰 ， 夏宏 ， 王 沁 微处理器浮点运算功能的测试 方法研究明 计算机工程与应用 ， ， 环二 ， ， ， 止 笔 ， ， ， 耐 ， ， ， ，