Voy a plantear una utilidad de las aserciones concurrentes para verificaci\u00f3n del buen hacer de vuestros dise\u00f1os de microprocesadores, sobre todo ahora que est\u00e1is uniendo vuestro bloques funcionales del single-cycle.<\/p>\n\n\n\n
Supongamos que teneis un core c\u00f3mo el que ahora os describo<\/p>\n\n\n\n
module CORE(\n\tinput CLK,\n\tinput RESET_N,\n\tinput [31:0] idata,ddata_r,\n\toutput [31:0] ddata_w,\n\toutput wire [31:0] iaddr, daddr,\n\toutput d_rw\n);\n\nwire [3:0]Instruction3, ALU_OPERATION;\nwire Zero,BranchMux,RegWrite,LUISrc,ALUSrc,MemtoReg,JumpRD,JumpPC;\n\nCONTROL_PATH controlPath(\n\t.Instruction(idata[6:0]),\n\t.InstructionFunct3({idata[30],idata[14:12]}),\n\t.ALUresult(daddr[0]),\/\/Bit para decidir salto mayor y menor.\n\t.*\n);\n\nDATA_PATH dataPath(\n\t.*\n);\n\nendmodule<\/pre><\/div>\n\n\n\nPensad que posiblemente dentro del DATA_PATH teng\u00e1is el banco de registros con un nombre de instanciaci\u00f3n RF1, y supongamos que la variable interna del registro la hemos llamado<\/p>\n\n\n\n
logic [31:0] aux [31:0];<\/pre><\/div>\n\n\n\n Vamos a incluir una aserci\u00f3n que nos permita verificar una de mis operaciones de R_format: la ADD.<\/p>\n\n\n\n
<\/p>\n\n\n\n
Puesto que verilog\/systemverilog puede acceder a cualquier variable de todo el dise\u00f1o a trav\u00e9s de su path jer\u00e1rquico, podemos acceder perfectamente desde el \u00abcore\u00bb que acabamos de visualizar. El siguiente c\u00f3digo nos permite detectar fallos (si los hubiera) en la ejecuci\u00f3n de dicha instrucci\u00f3n y de paso dar visibilidad en caso de error, de detalles sobre lo que deber\u00edamos obtener y que obtenemos realmente.<\/p>\n\n\n\n
sequence no_s0;\n logic [31:0] src1,src2;\n logic [4:0] add_destino;\n ({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));\nendsequence\nsequence s0;\n logic [31:0] src1,src2;\n logic [4:0] add_destino;\n ({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 );\nendsequence\nidea1: 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 )\nelse $error(\"R format add\");\nidea2: 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 );\n<\/pre><\/div>\n\n\n\n La idea es que si todo va bien, no aparezca ning\u00fan mensaje.<\/p>\n\n\n\n
Si la instrucci\u00f3n fallara en vuestro \u00abcore\u00bb, aparecer\u00eda un mensaje de error con el mensaje \u00abR format add\u00bb fruto de la aserci\u00f3n. Para tener detalles del error he incluido un cover property que tiene la misma sintaxis que las assert property y que est\u00e1 chequeando justamente la condici\u00f3n contraria a la correcta. Por tanto se ejecutar\u00eda y sacar\u00eda por pantalla un display con la suficiente informaci\u00f3n para saber en qu\u00e9 consiste el error. <\/p>\n\n\n\n
La secuencia correcta la hemos llamado s0 y la incorrecta no_s0<\/p>\n","protected":false},"excerpt":{"rendered":"
Voy a plantear una utilidad de las aserciones concurrentes para verificaci\u00f3n del buen hacer de vuestros dise\u00f1os de microprocesadores, sobre todo ahora que est\u00e1is uniendo vuestro bloques funcionales del single-cycle. Supongamos que teneis un core c\u00f3mo el que ahora os describo Pensad que posiblemente dentro del DATA_PATH teng\u00e1is el banco de registros con un nombre de instanciaci\u00f3n RF1, y supongamos que la variable interna del registro la hemos llamado Vamos a incluir una aserci\u00f3n 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\u00f1o a trav\u00e9s de su path jer\u00e1rquico, podemos acceder perfectamente desde el \u00abcore\u00bb que acabamos de visualizar. El siguiente c\u00f3digo nos permite detectar fallos (si los hubiera) en la ejecuci\u00f3n de dicha instrucci\u00f3n y de paso dar visibilidad en caso de error, de detalles sobre lo que deber\u00edamos obtener y que obtenemos realmente. La idea es que si todo va bien, no aparezca ning\u00fan mensaje. Si la instrucci\u00f3n fallara en vuestro \u00abcore\u00bb, aparecer\u00eda un mensaje de error con el mensaje \u00abR format add\u00bb fruto de la aserci\u00f3n. Para tener detalles del error he incluido un cover property que tiene la misma sintaxis que las assert property y que est\u00e1 chequeando justamente la condici\u00f3n contraria a la correcta. Por tanto se ejecutar\u00eda y sacar\u00eda por pantalla un display con la suficiente informaci\u00f3n para saber en qu\u00e9 consiste el error. La secuencia correcta la hemos llamado s0 y la incorrecta no_s0<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_crdt_document":"","ub_ctt_via":"","footnotes":""},"categories":[37,5],"tags":[40,39,38],"class_list":["post-715","post","type-post","status-publish","format-standard","hentry","category-assert-base-verification-abv","category-verificacion","tag-local-variable","tag-property","tag-sequence"],"featured_image_src":null,"author_info":{"display_name":"ralfgad","author_link":"https:\/\/dsd.webs.upv.es\/?author=2"},"_links":{"self":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/posts\/715","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=715"}],"version-history":[{"count":4,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/posts\/715\/revisions"}],"predecessor-version":[{"id":722,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=\/wp\/v2\/posts\/715\/revisions\/722"}],"wp:attachment":[{"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=715"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=715"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/dsd.webs.upv.es\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=715"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}