发明名称 基于边界条件和自检查随机测试的CPU约束生成验证法
摘要 本发明涉及属于计算机自动验证技术领域的基于边界条件和自检查随机测试的CPU约束生成验证法。其具体实施模式是:随机测试环境中分别包含体系结构模型和RTL模型。体系结构模型是期望的处理器模型,它采用C模拟器实现,是作为标准参考模型存在的。RTL模型是将要进行测试和验证的模型,随机测试及验证的目的是测试RTL模型是否与体系结构模型一致。RTL模型和体系结构模型都能输出在每一个时钟周期的处理器状态,比较两个模型的处理器状态,就能判断两个模型是否一致。本发明具有体系结构独立的特点,能够很容易构建针对新的处理器体系结构的验证平台,使得验证速度和验证质量都有很大提高,也使建立的随机验证平台能作为贯穿处理器验证始终的一个工具。
申请公布号 CN100336032C 申请公布日期 2007.09.05
申请号 CN200410101821.0 申请日期 2004.12.24
申请人 清华大学 发明人 姚文斌;张悠慧;王惊雷
分类号 G06F11/36(2006.01) 主分类号 G06F11/36(2006.01)
代理机构 代理人
主权项 1、基于边界条件和自检查随机测试的CPU约束生成验证法,其特征在于,它是在微处理器中依次按以下步骤实现的:第1步:向微机中输入下述指令集所述指令集是由所有指令树组成的指令数组,而指令树是根据每条指令的语法拼成的,其中每一条指令含有:指令类型,表示该指令所属的部件类型;操作数数目,表示该指令的操作数数目;操作数表,它由该指令的操作数组成;每个操作数含有:操作数类型域、操作数范围、操作数当前值、边界条件值表及边界条件值的概率;其中,操作数类型有:寄存器类型、立即数类型、存储器地址类型;指令格式,它是汇编指令的语法表示;指令编码,表示该指令的机器码编码方式;指令约束,表示该指令的约束条件;存储器地址方位表,表示该指令所操作的存储器范围;异常表,表示该指令有关的异常源的开启和关闭;指令计数,表示对所生成指令计数;第2步:生成随机测试程序,它依次含有以下步骤:第2.1步:生成随机测试程序的初始化段:第2.1.1步:读取指令集中的约束条件,改变指令的约束,读取检查点的间隔,即自检粒度,它用指令条数来表示,检查点即程序中检查处理器状态的位置;第2.1.2步:判断是否需要边界测试:若:需要边界测试,则改变指令约束为边界条件约束;否则,转入第2.1.3步;第2.1.3步:初始化微处理器中的寄存器和存储器,形成随机测试程序的初始化段;第2.2步:生成随机测试程序的程序段;第2.2.1步:随机选择一条指令以及指令操作数;第2.2.2步:对指令进行约束验证:第2.2.2.1步:在各指令的操作数的边界条件值表中加入相应的边界值以及生成该边界值的概率;第2.2.2.2步:根据该边界值的概率,在该操作数的边界条件值表和操作数范围内随机选择一个操作数,生成一条指定概率的随机测试指令;第2.2.2.3步:在标准参考模型C模拟器中运行上述生成的随机测试指令,根据运行结构判断:若:生成的指令是有效的,则转入第2.2.3步;否则:转入第2.2.1步;第2.2.3步:对第2.2.2步形成的基于边界条件的随机测试指令,自动生成自检查随机测试程序:第2.2.3.1步:在不同的测试阶段并根据不同的测试目的,设定下述自检查代码插入检查点位置;第2.2.3.2步:记录各检查点的处理器的当前状态,即寄存器状态和存储器状态,对于下一个检查点来说,当前记录的这个状态称为历史状态;第2.2.3.3步:记录各检查点在指令集中的当前位置,从中选取确定一个检查点,根据用户的要求,是只比较发生变化的寄存器或存储器,还是比较所有的寄存器和存储器,判断比较的方式:若:用户只要求比较发生变化的寄存器或存储器,则找出当前检查点与上一个检查点发生变化的寄存器或存储器,把变化的寄存器或存储器作为自检查的对象;否则,就是比较所有的寄存器和存储器,把当前的处理器状态,即寄存器和存储器状态,作为比较的对象,记录当前检查点的处理器状态;第2.2.3.4步:生成自检代码:取出当前处理器状态的值,即需要进行自检查的寄存器和存储器当前状态值,将这些值与在标准参考模型C模拟器运行到同一点得出的值进行比较,判断值是否相等;若:相等,则转第2.2.4步;否则:增加跳转指令,跳转的地址由用户指定,转到第2.2.4步;第2.2.4步:判断是否达到最大指令数;若:已经达到,则转第2.3步;否则,转第2.2.1步;第2.3步:生成随机测试程序的结束段:第2.3.1步:生成随机测试程序的结束代码,包含:顺序指令,它是当程序段中的一些转移指令,其跳转目标地址超过程序段的最后一条指令时,预先避免程序进入一个不确定的状态时而提出的;第2.3.2步:若在生成过程中增加了自检查指令,则生成标志检查成功或者失败的代码;第3步:将上述生成的测试程序写入文件中,该文件称为测试文件;第4步:在RTL模拟器中验证微处理器的功能和实现:第4.1步:从测试文件取出一条指令;第4.2步:把该条指令在RTL模拟器上运行,判断该指令是否是自检查指令:若:是自检查指令,将得到的处理器当前状态值和记录在测试程序中运行到该点的处理器状态值进行比较;否则,转第4.3步;第4.3步:将测试验证结果记录;第4.4步:判断测试程序是否结束:若:测试程序结束,则验证过程结束;否则,转第4.1步。
地址 100084北京市100084-82信箱