Verilog Mux 模块的 SV 断言验证 - 使用 SystemVerilog Assert Property

module mux(\n input sel1, sel2, sel3,\n input [15:0] in1, in2, in3,\n output [15:0] sel_reg_out\n);\n wire sel1, sel2, sel3;\n wire [15:0] in1, in2, in3;\n wire [15:0] sel_out;\n reg [15:0] sel_reg_out;\nassign sel_out = ({16{sel1}} & in1) | ({16{sel2}} & in2) | ({16{sel3}} & in3);\nalways @(posedge clk or negedge rst)\n if(!rst) sel_reg_out <= 'h0;\n else sel_reg_out <= sel_out;\nendmodule\n针对该模块写一个SV断言内容：可以使用SystemVerilog的assert property语句来编写断言。根据给定的模块，我们可以编写以下断言：\n\nsystemverilog\nmodule mux_assertion;\n reg sel1, sel2, sel3;\n reg [15:0] in1, in2, in3;\n wire [15:0] sel_reg_out;\n \n // Instantiate the DUT\n mux dut (\n .sel1(sel1),\n .sel2(sel2),\n .sel3(sel3),\n .in1(in1),\n .in2(in2),\n .in3(in3),\n .sel_reg_out(sel_reg_out)\n );\n \n // Assert that sel_reg_out is always equal to sel_out\n // when sel1, sel2, and sel3 are high\n // and in1, in2, and in3 are not all zeros\n assert property (\n @(posedge clk) disable iff (!rst)\n (sel1 && sel2 && sel3 && (in1 !== 16'h0) && (in2 !== 16'h0) && (in3 !== 16'h0))\n |-> (sel_reg_out == ((16'b1111_1111_1111_1111 & in1) |\n (16'b1111_1111_1111_1111 & in2) |\n (16'b1111_1111_1111_1111 & in3)))\n );\n \n // Add additional assertions if needed\n \nendmodule\n\n\n在上述断言中，我们使用assert property语句来表示断言条件。断言条件被指定为在时钟上升沿时成立的条件。在条件中，我们检查sel1、sel2和sel3是否都为高电平，并且in1、in2和in3是否都不为零。如果满足这些条件，则断言sel_reg_out的值应该等于(sel1 & in1) | (sel2 & in2) | (sel3 & in3)。\n\n请注意，上述代码中需要提供时钟信号clk和复位信号rst。如果需要，可以根据实际情况进行适当的修改。