面向寄存器的流水线处理器建模及验证方法

A Register-Oriented Modeling and Verification Method for Pipeline Microprocessor

提出了一种新的流水线处理器功能的验证方法 ,这种方法的主要思想是通过验证流水线处理器中所有寄存器的功能来验证处理器的功能 .流水线处理器绝大部分是由同步电路组成的 ,同步电路的状态则完全由寄存器的状态决定 ,因此如果能够保证每个寄存器功能正确就可以保证整个同步电路功能正确 .对于流水线处理器来说 ,寄存器状态的变迁是由处理器的原始输入和寄存器本身状态决定的 .原始输入包括控制信号 (如复位信号 )和数据输入 (如指令输入 ) .如果把对每个寄存器的赋值操作转换成对控制信号和数据输入的操作 ,就可以生成一个验证序列 ,这个序列包括每个时钟周期控制信号和数据输入的值 .有了这个序列就可以把目标设计和参考模型进行结果比较 ,从而验证目标设计功能是否正确 .同时这种方法也便于调试 .

A new function verification method,register-oriented function verification method for pipeline microprocessor is presented.The main idea of the verification method is that verifying the function of each register to prove that the function of the whole design is correct.The pipeline microprocessors are almost made up of synchronous circuits.The current state of the synchronous circuits is decided by the state of registers.If the function of every register is correct,the function of the whole synchronous circuits is also correct.The state transfer of registers lies on the state of registers themselves and the primary input of the synchronous circuits.But in the final analysis,the state transfer of registers is decided by the primary input.This method can find an input data sequence to verify the function of all registers by comparing the response of the circuits under verifying and its reference model.The method is fit for debugging very much.