Voy a plantear una utilidad de las aserciones concurrentes para verificación del buen hacer de vuestros diseños de microprocesadores, sobre todo ahora que estáis uniendo vuestro bloques funcionales del single-cycle.
Supongamos que teneis un core cómo el que ahora os describo
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 |
module CORE( input CLK, input RESET_N, input [31:0] idata,ddata_r, output [31:0] ddata_w, output wire [31:0] iaddr, daddr, output d_rw ); wire [3:0]Instruction3, ALU_OPERATION; wire Zero,BranchMux,RegWrite,LUISrc,ALUSrc,MemtoReg,JumpRD,JumpPC; CONTROL_PATH controlPath( .Instruction(idata[6:0]), .InstructionFunct3({idata[30],idata[14:12]}), .ALUresult(daddr[0]),//Bit para decidir salto mayor y menor. .* ); DATA_PATH dataPath( .* ); endmodule |
Pensad que posiblemente dentro del DATA_PATH tengáis el banco de registros con un nombre de instanciación RF1, y supongamos que la variable interna del registro la hemos llamado
|
1 |
logic [31:0] aux [31:0]; |
Vamos a incluir una aserción que nos permita verificar una de mis operaciones de R_format: la ADD.
Puesto que verilog/systemverilog puede acceder a cualquier variable de todo el diseño a través de su path jerárquico, podemos acceder perfectamente desde el «core» que acabamos de visualizar. El siguiente código nos permite detectar fallos (si los hubiera) en la ejecución de dicha instrucción y de paso dar visibilidad en caso de error, de detalles sobre lo que deberíamos obtener y que obtenemos realmente.
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
sequence no_s0; logic [31:0] src1,src2; logic [4:0] add_destino; ({idata[30],idata[14:12]}==4'b0000, src1=dataPath.RF1.aux[idata[19:15]], src2=dataPath.RF1.aux[idata[24:20]],add_destino=idata[11:7]) ##1 (dataPath.RF1.aux[add_destino]!=src1+src2, $display("en registro %d obtenido=%h esperado=%h",add_destino,dataPath.RF1.aux[add_destino],src1+src2)); endsequence sequence s0; logic [31:0] src1,src2; logic [4:0] add_destino; ({idata[30],idata[14:12]}==4'b0000, src1=dataPath.RF1.aux[idata[19:15]], src2=dataPath.RF1.aux[24:20]],add_destino=idata[11:7]) ##1 (dataPath.RF1.aux[add_destino]==src1+src2 ); endsequence idea1: assert property (@(posedge CLK) disable iff (RESET_N!=1'b1) idata[6:0]==7'b0110011&&idata[31]==1'b0&&idata[29:25]==5'b0000|->s0 ) else $error("R format add"); idea2: cover property (@(posedge CLK) disable iff (RESET_N!=1'b1) idata[6:0]==7'b0110011&&idata[31]==1'b0&&idata[29:25]==5'b0000|->no_s0 ); |
La idea es que si todo va bien, no aparezca ningún mensaje.
Si la instrucción fallara en vuestro «core», aparecería un mensaje de error con el mensaje «R format add» fruto de la aserción. Para tener detalles del error he incluido un cover property que tiene la misma sintaxis que las assert property y que está chequeando justamente la condición contraria a la correcta. Por tanto se ejecutaría y sacaría por pantalla un display con la suficiente información para saber en qué consiste el error.
La secuencia correcta la hemos llamado s0 y la incorrecta no_s0