[dv] Hard code various dv connections until full hook-up Signed-off-by: Timothy Chen <timothytim@google.com> [dv] more dv related fixes Signed-off-by: Timothy Chen <timothytim@google.com> [prim] Add auto generated fpv files Signed-off-by: Timothy Chen <timothytim@google.com>
diff --git a/hw/dv/sv/sim_sram/tlul_sink.sv b/hw/dv/sv/sim_sram/tlul_sink.sv index 771a084..5220931 100644 --- a/hw/dv/sv/sim_sram/tlul_sink.sv +++ b/hw/dv/sv/sim_sram/tlul_sink.sv
@@ -61,8 +61,8 @@ // Write mask should be all 1s. assign wr_mask_err = wr_req ? ~(&tl_i.a_mask) : 1'b0; - // Don't allow unsupported features. - assign malformed_meta_err = (tl_i.a_user.parity_en == 1'b1); + // Don't allow unsupported values. + assign malformed_meta_err = tl_a_user_chk(tl_i.a_user); // tl_err : separate checker tlul_err u_err (
diff --git a/hw/dv/sv/tl_agent/tl_host_driver.sv b/hw/dv/sv/tl_agent/tl_host_driver.sv index 9a1a807..37baf86 100644 --- a/hw/dv/sv/tl_agent/tl_host_driver.sv +++ b/hw/dv/sv/tl_agent/tl_host_driver.sv
@@ -107,7 +107,7 @@ cfg.vif.host_cb.h2d_int.a_param <= req.a_param; cfg.vif.host_cb.h2d_int.a_data <= req.a_data; cfg.vif.host_cb.h2d_int.a_mask <= req.a_mask; - cfg.vif.host_cb.h2d_int.a_user <= '0; + cfg.vif.host_cb.h2d_int.a_user <= tlul_pkg::TL_A_USER_DEFAULT; cfg.vif.host_cb.h2d_int.a_source <= req.a_source; cfg.vif.host_cb.h2d_int.a_valid <= 1'b1; end else begin
diff --git a/hw/ip/prim/fpv/prim_secded_64_57_fpv.core b/hw/ip/prim/fpv/prim_secded_64_57_fpv.core new file mode 100644 index 0000000..890cf29 --- /dev/null +++ b/hw/ip/prim/fpv/prim_secded_64_57_fpv.core
@@ -0,0 +1,33 @@ +CAPI=2: +# Copyright lowRISC contributors. +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 +name: "lowrisc:fpv:prim_secded_64_57_fpv:0.1" +description: "SECDED FPV target" +filesets: + files_formal: + depend: + - lowrisc:prim:all + - lowrisc:prim:secded + files: + - vip/prim_secded_64_57_assert_fpv.sv + - tb/prim_secded_64_57_fpv.sv + - tb/prim_secded_64_57_bind_fpv.sv + file_type: systemVerilogSource + +targets: + default: &default_target + # note, this setting is just used + # to generate a file list for jg + default_tool: icarus + filesets: + - files_formal + toplevel: + - prim_secded_64_57_fpv + + formal: + <<: *default_target + + lint: + <<: *default_target +
diff --git a/hw/ip/prim/fpv/tb/prim_secded_64_57_bind_fpv.sv b/hw/ip/prim/fpv/tb/prim_secded_64_57_bind_fpv.sv new file mode 100644 index 0000000..1ef65e2 --- /dev/null +++ b/hw/ip/prim/fpv/tb/prim_secded_64_57_bind_fpv.sv
@@ -0,0 +1,20 @@ +// Copyright lowRISC contributors. +// Licensed under the Apache License, Version 2.0, see LICENSE for details. +// SPDX-License-Identifier: Apache-2.0 +// +// SECDED FPV bind file generated by util/design/secded_gen.py + +module prim_secded_64_57_bind_fpv; + + bind prim_secded_64_57_fpv + prim_secded_64_57_assert_fpv prim_secded_64_57_assert_fpv ( + .clk_i, + .rst_ni, + .in, + .d_o, + .syndrome_o, + .err_o, + .error_inject_i + ); + +endmodule : prim_secded_64_57_bind_fpv
diff --git a/hw/ip/prim/fpv/tb/prim_secded_64_57_fpv.sv b/hw/ip/prim/fpv/tb/prim_secded_64_57_fpv.sv new file mode 100644 index 0000000..6827db7 --- /dev/null +++ b/hw/ip/prim/fpv/tb/prim_secded_64_57_fpv.sv
@@ -0,0 +1,31 @@ +// Copyright lowRISC contributors. +// Licensed under the Apache License, Version 2.0, see LICENSE for details. +// SPDX-License-Identifier: Apache-2.0 +// +// SECDED FPV testbench generated by util/design/secded_gen.py + +module prim_secded_64_57_fpv ( + input clk_i, + input rst_ni, + input [56:0] in, + output logic [56:0] d_o, + output logic [6:0] syndrome_o, + output logic [1:0] err_o, + input [63:0] error_inject_i +); + + logic [63:0] data_enc; + + prim_secded_64_57_enc prim_secded_64_57_enc ( + .in, + .out(data_enc) + ); + + prim_secded_64_57_dec prim_secded_64_57_dec ( + .in(data_enc ^ error_inject_i), + .d_o, + .syndrome_o, + .err_o + ); + +endmodule : prim_secded_64_57_fpv
diff --git a/hw/ip/prim/fpv/vip/prim_secded_64_57_assert_fpv.sv b/hw/ip/prim/fpv/vip/prim_secded_64_57_assert_fpv.sv new file mode 100644 index 0000000..ca9c830 --- /dev/null +++ b/hw/ip/prim/fpv/vip/prim_secded_64_57_assert_fpv.sv
@@ -0,0 +1,33 @@ +// Copyright lowRISC contributors. +// Licensed under the Apache License, Version 2.0, see LICENSE for details. +// SPDX-License-Identifier: Apache-2.0 +// +// SECDED FPV assertion file generated by util/design/secded_gen.py + +module prim_secded_64_57_assert_fpv ( + input clk_i, + input rst_ni, + input [56:0] in, + input [56:0] d_o, + input [6:0] syndrome_o, + input [1:0] err_o, + input [63:0] error_inject_i +); + + // Inject a maximum of two errors simultaneously. + `ASSUME_FPV(MaxTwoErrors_M, $countones(error_inject_i) <= 2) + // This bounds the input data state space to make sure the solver converges. + `ASSUME_FPV(DataLimit_M, $onehot0(in) || $onehot0(~in)) + // Single bit error detection + `ASSERT(SingleErrorDetect_A, $countones(error_inject_i) == 1 |-> err_o[0]) + `ASSERT(SingleErrorDetectReverse_A, err_o[0] |-> $countones(error_inject_i) == 1) + // Double bit error detection + `ASSERT(DoubleErrorDetect_A, $countones(error_inject_i) == 2 |-> err_o[1]) + `ASSERT(DoubleErrorDetectReverse_A, err_o[1] |-> $countones(error_inject_i) == 2) + // Single bit error correction (implicitly tests the syndrome output) + `ASSERT(SingleErrorCorrect_A, $countones(error_inject_i) < 2 |-> in == d_o) + // Basic syndrome check + `ASSERT(SyndromeCheck_A, |syndrome_o |-> $countones(error_inject_i) > 0) + `ASSERT(SyndromeCheckReverse_A, $countones(error_inject_i) > 0 |-> |syndrome_o) + +endmodule : prim_secded_64_57_assert_fpv
diff --git a/util/reggen/reg_top.sv.tpl b/util/reggen/reg_top.sv.tpl index 5f37a67..ebdbc6d 100644 --- a/util/reggen/reg_top.sv.tpl +++ b/util/reggen/reg_top.sv.tpl
@@ -313,7 +313,7 @@ // this is formulated as an assumption such that the FPV testbenches do disprove this // property by mistake - `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0) + //`ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.chk_en == tlul_pkg::CheckDis) endmodule <%def name="str_bits_sv(bits)">\