[dv/fpv] Clean up FPV script and add EndpointType to tlul_assert.sv This commit strives at eliminating some of the explicitly added demotions (from assert -> assume) in the fpv.tcl file. In particular, tlul_assert module contains now a parameter EndpointType that can either be set to "Host" or "Device", depending on what kind of endpoint it is bound to. Internally, some of the assertions are switched to assumptions based on that parameter. In order to keep code duplication to a minimum, the asserted/assumed sequences have been split out as discrete sequence items such that they are only declared once. The assertion enable/disable functions had to be revised as well, and the tlul_assert interface has been changed into a module. Further, two additional ASSUME macros have been added to prim_assert in order to support immediate assumptions, and the reqParity assertion in the register file is changed into an assumption everywhere. All FPV and DV testbenches have been adapted to use the proper EndpointType. Note that the behavior of the assertions/assumptions will remain the same for all DV sims, but it changes the way they behave in FPV.
diff --git a/hw/dv/sv/cip_lib/cip_base_env.sv b/hw/dv/sv/cip_lib/cip_base_env.sv index 6a1068a..f153fd8 100644 --- a/hw/dv/sv/cip_lib/cip_base_env.sv +++ b/hw/dv/sv/cip_lib/cip_base_env.sv
@@ -40,9 +40,9 @@ if (!uvm_config_db#(devmode_vif)::get(this, "", "devmode_vif", cfg.devmode_vif)) begin `uvm_fatal(get_full_name(), "failed to get devmode_vif from uvm_config_db") end - if (!uvm_config_db#(tlul_assert_vif)::get(this, "", "tlul_assert_vif", - cfg.tlul_assert_vif)) begin - `uvm_fatal(get_full_name(), "failed to get tlul_assert_vif from uvm_config_db") + if (!uvm_config_db#(tlul_assert_ctrl_vif)::get(this, "", "tlul_assert_ctrl_vif", + cfg.tlul_assert_ctrl_vif)) begin + `uvm_fatal(get_full_name(), "failed to get tlul_assert_ctrl_vif from uvm_config_db") end // create components
diff --git a/hw/dv/sv/cip_lib/cip_base_env_cfg.sv b/hw/dv/sv/cip_lib/cip_base_env_cfg.sv index 404870e..71490db 100644 --- a/hw/dv/sv/cip_lib/cip_base_env_cfg.sv +++ b/hw/dv/sv/cip_lib/cip_base_env_cfg.sv
@@ -10,7 +10,7 @@ intr_vif intr_vif; alerts_vif alerts_vif; devmode_vif devmode_vif; - tlul_assert_vif tlul_assert_vif; + tlul_assert_ctrl_vif tlul_assert_ctrl_vif; // only security IP can support devmode. If supported, override it to 1 in initialize() bit en_devmode = 0;
diff --git a/hw/dv/sv/cip_lib/cip_base_vseq__tl_errors.svh b/hw/dv/sv/cip_lib/cip_base_vseq__tl_errors.svh index e53853e..a79f3ea 100644 --- a/hw/dv/sv/cip_lib/cip_base_vseq__tl_errors.svh +++ b/hw/dv/sv/cip_lib/cip_base_vseq__tl_errors.svh
@@ -116,7 +116,7 @@ bit test_mem_err_byte_write = (cfg.mem_addrs.size > 0) && !cfg.en_mem_byte_write; bit test_mem_err_read = (cfg.mem_addrs.size > 0) && !cfg.en_mem_read; `uvm_info(`gfn, "Running run_tl_errors_vseq", UVM_LOW) - cfg.tlul_assert_vif.disable_sva_for_tl_errors(); + cfg.tlul_assert_ctrl_vif.drive(1'b0); for (int trans = 1; trans <= num_times; trans++) begin if (cfg.en_devmode == 1) begin @@ -138,7 +138,7 @@ join_none wait fork; end // for - cfg.tlul_assert_vif.enable_sva_for_tl_errors(); + cfg.tlul_assert_ctrl_vif.drive(1'b1); endtask : run_tl_errors_vseq `undef create_tl_access_error_case
diff --git a/hw/dv/sv/common_ifs/clk_rst_if.sv b/hw/dv/sv/common_ifs/clk_rst_if.sv index 0cad69e..559cc68 100644 --- a/hw/dv/sv/common_ifs/clk_rst_if.sv +++ b/hw/dv/sv/common_ifs/clk_rst_if.sv
@@ -19,10 +19,12 @@ inout rst_n ); +`ifndef VERILATOR // include macros and import pkgs `include "dv_macros.svh" `include "uvm_macros.svh" import uvm_pkg::*; +`endif bit drive_clk; // enable clk generation logic o_clk; // output clk @@ -81,7 +83,11 @@ drive_rst_n = drive_rst_n_val; end else begin +`ifdef VERILATOR + $error({msg_id, "this function can only be called at t=0"}); +`else `uvm_fatal(msg_id, "this function can only be called at t=0") +`endif end endfunction @@ -95,7 +101,11 @@ // set the duty cycle (1-99) function automatic void set_duty_cycle(int duty); if (!(duty inside {[1:99]})) begin +`ifdef VERILATOR + $error({msg_id, $sformatf("duty cycle %0d is not inside [1:99]", duty)}); +`else `uvm_fatal(msg_id, $sformatf("duty cycle %0d is not inside [1:99]", duty)) +`endif end duty_cycle = duty; recompute = 1'b1; @@ -110,7 +120,11 @@ // 0 - dont add any jitter; 100 - add jitter on every clock edge function automatic void set_jitter_chance_pc(int jitter_chance); if (!(jitter_chance inside {[0:100]})) begin +`ifdef VERILATOR + $error({msg_id, $sformatf("jitter_chance %0d is not inside [0:100]", jitter_chance)}); +`else `uvm_fatal(msg_id, $sformatf("jitter_chance %0d is not inside [0:100]", jitter_chance)) +`endif end jitter_chance_pc = jitter_chance; endfunction @@ -130,13 +144,17 @@ function automatic void add_jitter(); int jitter_ps; if ($urandom_range(1, 100) <= jitter_chance_pc) begin +`ifndef VERILATOR `DV_CHECK_STD_RANDOMIZE_WITH_FATAL(jitter_ps, jitter_ps inside {[-1*max_jitter_ps:max_jitter_ps]};, "", msg_id) +`endif clk_hi_ps += jitter_ps; end if ($urandom_range(1, 100) <= jitter_chance_pc) begin +`ifndef VERILATOR `DV_CHECK_STD_RANDOMIZE_WITH_FATAL(jitter_ps, jitter_ps inside {[-1*max_jitter_ps:max_jitter_ps]};, "", msg_id) +`endif clk_lo_ps += jitter_ps; end endfunction
diff --git a/hw/dv/sv/common_ifs/common_ifs.core b/hw/dv/sv/common_ifs/common_ifs.core index 05591b6..31ca693 100644 --- a/hw/dv/sv/common_ifs/common_ifs.core +++ b/hw/dv/sv/common_ifs/common_ifs.core
@@ -7,8 +7,9 @@ filesets: files_dv: + depend: + - lowrisc:dv:pins_if files: - - pins_if.sv - clk_if.sv - clk_rst_if.sv file_type: systemVerilogSource
diff --git a/hw/dv/sv/common_ifs/pins_if.sv b/hw/dv/sv/common_ifs/pins_if.sv index 2907926..62931cb 100644 --- a/hw/dv/sv/common_ifs/pins_if.sv +++ b/hw/dv/sv/common_ifs/pins_if.sv
@@ -82,7 +82,11 @@ // any 'x' value on pin, that may result due to conflicting values // between 'value to be driven out' and the external driver's value. assign pins[i] = pins_oe[i] ? pins_o[i] : 1'bz; +`ifdef VERILATOR + assign pins[i] = ~pins_oe[i] ? pins_int[i] : 1'bz; +`else assign (pull0, pull1) pins[i] = ~pins_oe[i] ? pins_int[i] : 1'bz; +`endif end endgenerate
diff --git a/hw/dv/sv/common_ifs/pins_ifs.core b/hw/dv/sv/common_ifs/pins_ifs.core new file mode 100644 index 0000000..f528e12 --- /dev/null +++ b/hw/dv/sv/common_ifs/pins_ifs.core
@@ -0,0 +1,17 @@ +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:dv:pins_if" +description: "Common interfaces used in DV" + +filesets: + files_dv: + files: + - pins_if.sv + file_type: systemVerilogSource + +targets: + default: + filesets: + - files_dv
diff --git a/hw/dv/sv/dv_utils/dv_utils_pkg.sv b/hw/dv/sv/dv_utils/dv_utils_pkg.sv index 50c19bd..6cef61c 100644 --- a/hw/dv/sv/dv_utils/dv_utils_pkg.sv +++ b/hw/dv/sv/dv_utils/dv_utils_pkg.sv
@@ -26,7 +26,7 @@ typedef virtual pins_if #(NUM_MAX_INTERRUPTS) intr_vif; typedef virtual pins_if #(NUM_MAX_ALERTS) alerts_vif; typedef virtual pins_if #(1) devmode_vif; - typedef virtual tlul_assert tlul_assert_vif; + typedef virtual pins_if #(1) tlul_assert_ctrl_vif; // interface direction / mode - Host or Device typedef enum bit {
diff --git a/hw/formal/fpv.tcl b/hw/formal/fpv.tcl index 6833222..45ed34c 100644 --- a/hw/formal/fpv.tcl +++ b/hw/formal/fpv.tcl
@@ -69,29 +69,6 @@ # assume properties for inputs #------------------------------------------------------------------------- -# For generated *_reg_top modules, below assertion solely depends on -# module inputs a_valid and a_user.parity_en, and therefore is -# assumed to be correct -assume -from_assert -remove_original -regexp {^\w*\.u_reg\.reqParity} - -# For all TL-UL host-interfaces (i.e. ports interfacing a host), A-channel is -# an input, so inputs a_opcode, a_param, etc. are constrained by below assuames. -# Note that all tlul_assert checkers for host interfaces are called tlul_assert_host* -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.legalAOpcode} -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.legalAParam} -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.sizeMatchesMask} -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.sizeGTEMask} -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.onlyOnePendingReqPerSourceID} -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.addressAlignedToSize} -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_host\w*\.maskMustBeContiguous} - -# For all TL-UL device-interfaces (i.e. ports interfacing a device), D-channel is an -# input, so inputs d_* are constrained by below assumes -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_device\w*\.checkResponseOpcode} -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_device\w*\.legalDParam} -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_device\w*\.responseSizeMustEqualReqSize} -assume -from_assert -remove_original -regexp {^\w*\.tlul_assert_device\w*\.responseMustHaveReq} - # Notes on above regular expressions: ^ indicates the beginning of the string; # \w* includes all letters a-z, A-Z, and the underscore, but not the period. # And \. is for period (with escape). These regular expressions make sure that
diff --git a/hw/ip/aes/rtl/aes_reg_top.sv b/hw/ip/aes/rtl/aes_reg_top.sv index 644c707..70207d0 100644 --- a/hw/ip/aes/rtl/aes_reg_top.sv +++ b/hw/ip/aes/rtl/aes_reg_top.sv
@@ -1021,6 +1021,6 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/alert_handler/dv/tb/alert_handler_bind.sv b/hw/ip/alert_handler/dv/tb/alert_handler_bind.sv index 2d134d6..0876d2f 100644 --- a/hw/ip/alert_handler/dv/tb/alert_handler_bind.sv +++ b/hw/ip/alert_handler/dv/tb/alert_handler_bind.sv
@@ -4,7 +4,9 @@ module alert_handler_bind; - bind alert_handler tlul_assert tlul_assert_host ( + bind alert_handler tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i),
diff --git a/hw/ip/alert_handler/dv/tb/tb.sv b/hw/ip/alert_handler/dv/tb/tb.sv index dae3ba9..ae66cf8 100644 --- a/hw/ip/alert_handler/dv/tb/tb.sv +++ b/hw/ip/alert_handler/dv/tb/tb.sv
@@ -101,8 +101,8 @@ uvm_config_db#(esc_en_vif)::set(null, "*.env", "esc_en_vif", esc_en_if); uvm_config_db#(entropy_vif)::set(null, "*.env", "entropy_vif", entropy_if); uvm_config_db#(devmode_vif)::set(null, "*.env", "devmode_vif", devmode_if); - uvm_config_db#(tlul_assert_vif)::set(null, "*.env", "tlul_assert_vif", - tb.dut.tlul_assert_host); + uvm_config_db#(tlul_assert_ctrl_vif)::set(null, "*.env", "tlul_assert_ctrl_vif", + dut.tlul_assert_device.tlul_assert_ctrl_if); uvm_config_db#(virtual tl_if)::set(null, "*.env.m_tl_agent*", "vif", tl_if); $timeformat(-12, 0, " ps", 12); run_test();
diff --git a/hw/ip/alert_handler/rtl/alert_handler_reg_top.sv b/hw/ip/alert_handler/rtl/alert_handler_reg_top.sv index f1bc627..14a4c8f 100644 --- a/hw/ip/alert_handler/rtl/alert_handler_reg_top.sv +++ b/hw/ip/alert_handler/rtl/alert_handler_reg_top.sv
@@ -4302,6 +4302,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/flash_ctrl/dv/tb/flash_ctrl_bind.sv b/hw/ip/flash_ctrl/dv/tb/flash_ctrl_bind.sv index fc04606..2482c04 100644 --- a/hw/ip/flash_ctrl/dv/tb/flash_ctrl_bind.sv +++ b/hw/ip/flash_ctrl/dv/tb/flash_ctrl_bind.sv
@@ -4,7 +4,9 @@ module flash_ctrl_bind; - bind flash_ctrl tlul_assert tlul_assert_host ( + bind flash_ctrl tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i),
diff --git a/hw/ip/flash_ctrl/rtl/flash_ctrl_reg_top.sv b/hw/ip/flash_ctrl/rtl/flash_ctrl_reg_top.sv index 7a8dc1f..6b52812 100644 --- a/hw/ip/flash_ctrl/rtl/flash_ctrl_reg_top.sv +++ b/hw/ip/flash_ctrl/rtl/flash_ctrl_reg_top.sv
@@ -3384,6 +3384,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/gpio/dv/tb/gpio_bind.sv b/hw/ip/gpio/dv/tb/gpio_bind.sv index d54ead5..ee3647c 100644 --- a/hw/ip/gpio/dv/tb/gpio_bind.sv +++ b/hw/ip/gpio/dv/tb/gpio_bind.sv
@@ -4,7 +4,9 @@ module gpio_bind; - bind gpio tlul_assert tlul_assert_host ( + bind gpio tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i),
diff --git a/hw/ip/gpio/dv/tb/tb.sv b/hw/ip/gpio/dv/tb/tb.sv index d23aab3..f099987 100644 --- a/hw/ip/gpio/dv/tb/tb.sv +++ b/hw/ip/gpio/dv/tb/tb.sv
@@ -66,8 +66,8 @@ uvm_config_db#(intr_vif)::set(null, "*.env", "intr_vif", intr_if); uvm_config_db#(alerts_vif)::set(null, "*.env", "alerts_vif", alerts_if); uvm_config_db#(devmode_vif)::set(null, "*.env", "devmode_vif", devmode_if); - uvm_config_db#(tlul_assert_vif)::set(null, "*.env", "tlul_assert_vif", - tb.dut.tlul_assert_host); + uvm_config_db#(tlul_assert_ctrl_vif)::set(null, "*.env", "tlul_assert_ctrl_vif", + dut.tlul_assert_device.tlul_assert_ctrl_if); uvm_config_db#(virtual tl_if)::set(null, "*.env.m_tl_agent*", "vif", tl_if); uvm_config_db#(virtual pins_if #(NUM_GPIOS))::set(null, "*.env", "gpio_vif", gpio_if); $timeformat(-12, 0, " ps", 12);
diff --git a/hw/ip/gpio/rtl/gpio_reg_top.sv b/hw/ip/gpio/rtl/gpio_reg_top.sv index 01f151e..0827d82 100644 --- a/hw/ip/gpio/rtl/gpio_reg_top.sv +++ b/hw/ip/gpio/rtl/gpio_reg_top.sv
@@ -711,6 +711,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/hmac/dv/env/hmac_env.sv b/hw/ip/hmac/dv/env/hmac_env.sv index 397a625..c6b3438 100644 --- a/hw/ip/hmac/dv/env/hmac_env.sv +++ b/hw/ip/hmac/dv/env/hmac_env.sv
@@ -11,6 +11,11 @@ function void build_phase(uvm_phase phase); super.build_phase(phase); + // get vifs + if (!uvm_config_db#(d2h_a_ready_vif)::get(this, "", "d2h_a_ready_vif", + cfg.d2h_a_ready_vif)) begin + `uvm_fatal(get_full_name(), "failed to get d2h_a_ready_vif from uvm_config_db") + end endfunction endclass
diff --git a/hw/ip/hmac/dv/env/hmac_env_cfg.sv b/hw/ip/hmac/dv/env/hmac_env_cfg.sv index 9e4a2e8..91bef16 100644 --- a/hw/ip/hmac/dv/env/hmac_env_cfg.sv +++ b/hw/ip/hmac/dv/env/hmac_env_cfg.sv
@@ -6,6 +6,8 @@ `uvm_object_utils(hmac_env_cfg) `uvm_object_new + d2h_a_ready_vif d2h_a_ready_vif; + virtual function void initialize_csr_addr_map_size(); this.csr_addr_map_size = HMAC_ADDR_MAP_SIZE; endfunction : initialize_csr_addr_map_size
diff --git a/hw/ip/hmac/dv/env/hmac_env_pkg.sv b/hw/ip/hmac/dv/env/hmac_env_pkg.sv index b4c1cdb..483e339 100644 --- a/hw/ip/hmac/dv/env/hmac_env_pkg.sv +++ b/hw/ip/hmac/dv/env/hmac_env_pkg.sv
@@ -65,6 +65,7 @@ typedef class hmac_env_cfg; typedef class hmac_env_cov; typedef cip_base_virtual_sequencer #(hmac_env_cfg, hmac_env_cov) hmac_virtual_sequencer; + typedef virtual pins_if #(1) d2h_a_ready_vif; // functions
diff --git a/hw/ip/hmac/dv/env/hmac_scoreboard.sv b/hw/ip/hmac/dv/env/hmac_scoreboard.sv index 96540be..bfc7539 100644 --- a/hw/ip/hmac/dv/env/hmac_scoreboard.sv +++ b/hw/ip/hmac/dv/env/hmac_scoreboard.sv
@@ -65,7 +65,7 @@ foreach (msg[i]) begin msg_q.push_back(msg[i]); if (msg_q.size() % 4 == 0) begin - wait(cfg.tlul_assert_vif.d2h.a_ready == 1); // wait for outstanding transaction + wait(cfg.d2h_a_ready_vif.sample() == 1); // wait for outstanding transaction incr_wr_and_check_fifo_full(); end end
diff --git a/hw/ip/hmac/dv/tb/hmac_bind.sv b/hw/ip/hmac/dv/tb/hmac_bind.sv index 68bebfc..fc7ef4c 100644 --- a/hw/ip/hmac/dv/tb/hmac_bind.sv +++ b/hw/ip/hmac/dv/tb/hmac_bind.sv
@@ -4,11 +4,14 @@ module hmac_bind; - bind hmac tlul_assert tlul_assert_host ( + bind hmac tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i), .d2h (tl_o) ); + endmodule
diff --git a/hw/ip/hmac/dv/tb/tb.sv b/hw/ip/hmac/dv/tb/tb.sv index da81b76..3bc4db7 100644 --- a/hw/ip/hmac/dv/tb/tb.sv +++ b/hw/ip/hmac/dv/tb/tb.sv
@@ -29,6 +29,7 @@ pins_if #(NUM_MAX_ALERTS) alerts_if(.pins(alerts)); pins_if #(1) devmode_if(devmode); tl_if tl_if(.clk(clk), .rst_n(rst_n)); + pins_if #(1) d2h_a_ready_if(tl_if.d2h.a_ready); // dut hmac dut ( @@ -54,8 +55,9 @@ uvm_config_db#(intr_vif)::set(null, "*.env", "intr_vif", intr_if); uvm_config_db#(alerts_vif)::set(null, "*.env", "alerts_vif", alerts_if); uvm_config_db#(devmode_vif)::set(null, "*.env", "devmode_vif", devmode_if); - uvm_config_db#(tlul_assert_vif)::set(null, "*.env", "tlul_assert_vif", - tb.dut.tlul_assert_host); + uvm_config_db#(tlul_assert_ctrl_vif)::set(null, "*.env", "tlul_assert_ctrl_vif", + dut.tlul_assert_device.tlul_assert_ctrl_if); + uvm_config_db#(d2h_a_ready_vif)::set(null, "*.env", "d2h_a_ready_vif", d2h_a_ready_if); uvm_config_db#(virtual tl_if)::set(null, "*.env.m_tl_agent*", "vif", tl_if); $timeformat(-12, 0, " ps", 12); run_test();
diff --git a/hw/ip/hmac/rtl/hmac_reg_top.sv b/hw/ip/hmac/rtl/hmac_reg_top.sv index 8531024..23ff205 100644 --- a/hw/ip/hmac/rtl/hmac_reg_top.sv +++ b/hw/ip/hmac/rtl/hmac_reg_top.sv
@@ -1323,6 +1323,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/i2c/dv/tb/i2c_bind.sv b/hw/ip/i2c/dv/tb/i2c_bind.sv index 174baff..b9e3d6c 100644 --- a/hw/ip/i2c/dv/tb/i2c_bind.sv +++ b/hw/ip/i2c/dv/tb/i2c_bind.sv
@@ -4,11 +4,14 @@ module i2c_bind; - bind i2c tlul_assert tlul_assert_host ( + bind i2c tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i), .d2h (tl_o) ); + endmodule
diff --git a/hw/ip/i2c/dv/tb/tb.sv b/hw/ip/i2c/dv/tb/tb.sv index 6e651a3..e5912ff 100644 --- a/hw/ip/i2c/dv/tb/tb.sv +++ b/hw/ip/i2c/dv/tb/tb.sv
@@ -79,8 +79,8 @@ uvm_config_db#(intr_vif)::set(null, "*.env", "intr_vif", intr_if); uvm_config_db#(alerts_vif)::set(null, "*.env", "alerts_vif", alerts_if); uvm_config_db#(devmode_vif)::set(null, "*.env", "devmode_vif", devmode_if); - uvm_config_db#(tlul_assert_vif)::set(null, "*.env", "tlul_assert_vif", - tb.dut.tlul_assert_host); + uvm_config_db#(tlul_assert_ctrl_vif)::set(null, "*.env", "tlul_assert_ctrl_vif", + dut.tlul_assert_device.tlul_assert_ctrl_if); uvm_config_db#(virtual tl_if)::set(null, "*.env.m_tl_agent*", "vif", tl_if); uvm_config_db#(virtual i2c_if)::set(null, "*.env.m_i2c_agent*", "vif", i2c_if); $timeformat(-12, 0, " ps", 12);
diff --git a/hw/ip/i2c/rtl/i2c_reg_top.sv b/hw/ip/i2c/rtl/i2c_reg_top.sv index 86e99d9..4d5ee57 100644 --- a/hw/ip/i2c/rtl/i2c_reg_top.sv +++ b/hw/ip/i2c/rtl/i2c_reg_top.sv
@@ -2065,6 +2065,6 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/padctrl/fpv/padctrl_fpv.core b/hw/ip/padctrl/fpv/padctrl_fpv.core index e43445e..85996b9 100644 --- a/hw/ip/padctrl/fpv/padctrl_fpv.core +++ b/hw/ip/padctrl/fpv/padctrl_fpv.core
@@ -7,6 +7,7 @@ filesets: files_fpv: depend: + - lowrisc:ip:tlul - lowrisc:ip:padctrl - lowrisc:prim:prim_pkg files:
diff --git a/hw/ip/padctrl/fpv/tb/padctrl_bind.sv b/hw/ip/padctrl/fpv/tb/padctrl_bind.sv index 564c8af..fbf152e 100644 --- a/hw/ip/padctrl/fpv/tb/padctrl_bind.sv +++ b/hw/ip/padctrl/fpv/tb/padctrl_bind.sv
@@ -15,4 +15,13 @@ .* ); + bind padctrl tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( + .clk_i, + .rst_ni, + .h2d (tl_i), + .d2h (tl_o) + ); + endmodule : padctrl_bind
diff --git a/hw/ip/padctrl/rtl/padctrl_reg_top.sv b/hw/ip/padctrl/rtl/padctrl_reg_top.sv index 7ff61f9..e0b6ee6 100644 --- a/hw/ip/padctrl/rtl/padctrl_reg_top.sv +++ b/hw/ip/padctrl/rtl/padctrl_reg_top.sv
@@ -686,6 +686,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/pinmux/fpv/pinmux_fpv.core b/hw/ip/pinmux/fpv/pinmux_fpv.core index 88f5de5..5f01ff8 100644 --- a/hw/ip/pinmux/fpv/pinmux_fpv.core +++ b/hw/ip/pinmux/fpv/pinmux_fpv.core
@@ -7,6 +7,7 @@ filesets: files_fpv: depend: + - lowrisc:ip:tlul - lowrisc:ip:pinmux files: - tb/pinmux_tb.sv
diff --git a/hw/ip/pinmux/fpv/tb/pinmux_bind.sv b/hw/ip/pinmux/fpv/tb/pinmux_bind.sv index f60944b..844aa29 100644 --- a/hw/ip/pinmux/fpv/tb/pinmux_bind.sv +++ b/hw/ip/pinmux/fpv/tb/pinmux_bind.sv
@@ -13,4 +13,13 @@ .* ); + bind pinmux tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( + .clk_i, + .rst_ni, + .h2d (tl_i), + .d2h (tl_o) + ); + endmodule : pinmux_bind
diff --git a/hw/ip/pinmux/rtl/pinmux_reg_top.sv b/hw/ip/pinmux/rtl/pinmux_reg_top.sv index cd0958d..d1dd6a0 100644 --- a/hw/ip/pinmux/rtl/pinmux_reg_top.sv +++ b/hw/ip/pinmux/rtl/pinmux_reg_top.sv
@@ -969,6 +969,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/prim/rtl/prim_assert.sv b/hw/ip/prim/rtl/prim_assert.sv index b6fb9a2..23ae0b5 100644 --- a/hw/ip/prim/rtl/prim_assert.sv +++ b/hw/ip/prim/rtl/prim_assert.sv
@@ -159,6 +159,15 @@ else begin `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) end \ `endif +// Assume an immediate property +`define ASSUME_I(__name, __prop) \ +`ifndef VERILATOR \ + //pragma translate_off \ + __name: assume (__prop) \ + else `ASSERT_RPT(`PRIM_STRINGIFY(__name), `PRIM_STRINGIFY(__prop)) \ + //pragma translate_on \ +`endif + ////////////////////////////////// // For formal verification only // ////////////////////////////////// @@ -173,6 +182,13 @@ `ASSUME(__name, __prop, __clk, __rst) \ `endif +// ASSUME_I_FPV +// Assume a concurrent property during formal verification only. +`define ASSUME_I_FPV(__name, __prop) \ +`ifdef FPV_ON \ + `ASSUME_I(__name, __prop) \ +`endif + // COVER_FPV // Cover a concurrent property during formal verification `define COVER_FPV(__name, __prop, __clk, __rst) \
diff --git a/hw/ip/rv_core_ibex/dv/tb/core_ibex_bind.sv b/hw/ip/rv_core_ibex/dv/tb/core_ibex_bind.sv new file mode 100644 index 0000000..ed97d0d --- /dev/null +++ b/hw/ip/rv_core_ibex/dv/tb/core_ibex_bind.sv
@@ -0,0 +1,25 @@ +// Copyright lowRISC contributors. +// Licensed under the Apache License, Version 2.0, see LICENSE for details. +// SPDX-License-Identifier: Apache-2.0 + +module core_ibex_bind; + + bind rv_core_ibex tlul_assert #( + .EndpointType("Host") + ) tlul_assert_host_instr ( + .clk_i, + .rst_ni, + .h2d (tl_i_o), + .d2h (tl_i_i) + ); + + bind rv_core_ibex tlul_assert #( + .EndpointType("Host") + ) tlul_assert_host_data ( + .clk_i, + .rst_ni, + .h2d (tl_d_o), + .d2h (tl_d_i) + ); + +endmodule
diff --git a/hw/ip/rv_dm/dv/tb/rv_dm_bind.sv b/hw/ip/rv_dm/dv/tb/rv_dm_bind.sv index 50526be..8739ba2 100644 --- a/hw/ip/rv_dm/dv/tb/rv_dm_bind.sv +++ b/hw/ip/rv_dm/dv/tb/rv_dm_bind.sv
@@ -4,14 +4,18 @@ module rv_dm_bind; - bind rv_dm tlul_assert tlul_assert_host ( + bind rv_dm tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_d_i), .d2h (tl_d_o) ); - bind rv_dm tlul_assert tlul_assert_device ( + bind rv_dm tlul_assert #( + .EndpointType("Host") + ) tlul_assert_host ( .clk_i, .rst_ni, .h2d (tl_h_o),
diff --git a/hw/ip/rv_dm/rtl/deps.f b/hw/ip/rv_dm/rtl/deps.f index c00b567..7f17194 100644 --- a/hw/ip/rv_dm/rtl/deps.f +++ b/hw/ip/rv_dm/rtl/deps.f
@@ -1,10 +1,14 @@ +${PRJ_DIR}/hw/top_earlgrey/rtl/top_pkg.sv +${PRJ_DIR}/hw/ip/tlul/rtl/tlul_pkg.sv +${PRJ_DIR}/hw/ip/prim/rtl/prim_pkg.sv + ${PRJ_DIR}/hw/ip/prim/rtl/prim_assert.sv ${PRJ_DIR}/hw/ip/prim/rtl/prim_flop_2sync.sv ${PRJ_DIR}/hw/ip/prim/rtl/prim_fifo_async.sv ${PRJ_DIR}/hw/ip/prim/rtl/prim_fifo_sync.sv - -${PRJ_DIR}/hw/ip/tlul/rtl/top_pkg.sv -${PRJ_DIR}/hw/ip/tlul/rtl/tlul_pkg.sv +${PRJ_DIR}/hw/ip/prim/rtl/prim_clock_inverter.sv +${PRJ_DIR}/hw/ip/prim/abstract/prim_clock_mux2.sv +${PRJ_DIR}/hw/ip/prim_generic/rtl/prim_generic_clock_mux2.sv ${PRJ_DIR}/hw/vendor/pulp_riscv_dbg/src/dm_pkg.sv ${PRJ_DIR}/hw/vendor/pulp_riscv_dbg/debug_rom/debug_rom.sv @@ -15,3 +19,4 @@ ${PRJ_DIR}/hw/vendor/pulp_riscv_dbg/src/dmi_jtag.sv ${PRJ_DIR}/hw/vendor/pulp_riscv_dbg/src/dmi_jtag_tap.sv ${PRJ_DIR}/hw/ip/tlul/rtl/tlul_adapter_sram.sv +${PRJ_DIR}/hw/ip/tlul/rtl/tlul_err.sv
diff --git a/hw/ip/rv_plic/dv/rv_plic_bind.sv b/hw/ip/rv_plic/dv/rv_plic_bind.sv index 56cca60..1747af0 100644 --- a/hw/ip/rv_plic/dv/rv_plic_bind.sv +++ b/hw/ip/rv_plic/dv/rv_plic_bind.sv
@@ -4,7 +4,9 @@ module rv_plic_bind; - bind rv_plic tlul_assert tlul_assert_host ( + bind rv_plic tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i),
diff --git a/hw/ip/rv_plic/fpv/rv_plic.core b/hw/ip/rv_plic/fpv/rv_plic.core index f5fe6ff..db96d4a 100644 --- a/hw/ip/rv_plic/fpv/rv_plic.core +++ b/hw/ip/rv_plic/fpv/rv_plic.core
@@ -10,11 +10,8 @@ depend: - lowrisc:ip:tlul - lowrisc:prim:all - - lowrisc:ip:rv_plic_component + - lowrisc:ip:rv_plic_example files: - - ../rtl/rv_plic_reg_pkg.sv - - ../rtl/rv_plic_reg_top.sv - - ../rtl/rv_plic.sv - tb/rv_plic_bind.sv - vip/rv_plic_assert.sv file_type: systemVerilogSource @@ -22,7 +19,7 @@ targets: default: &default_target toplevel: - - ../rtl/rv_plic.sv + - rv_plic filesets: - files_fpv default_tool: jg
diff --git a/hw/ip/rv_plic/fpv/tb/rv_plic_bind.sv b/hw/ip/rv_plic/fpv/tb/rv_plic_bind.sv index 932a808..cf03038 100644 --- a/hw/ip/rv_plic/fpv/tb/rv_plic_bind.sv +++ b/hw/ip/rv_plic/fpv/tb/rv_plic_bind.sv
@@ -11,7 +11,9 @@ .irq_id_o, .msip_o ); - bind rv_plic tlul_assert tlul_assert_host( + bind rv_plic tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d(tl_i),
diff --git a/hw/ip/rv_plic/rtl/rv_plic_reg_top.sv b/hw/ip/rv_plic/rtl/rv_plic_reg_top.sv index 201cbfd..12279d6 100644 --- a/hw/ip/rv_plic/rtl/rv_plic_reg_top.sv +++ b/hw/ip/rv_plic/rtl/rv_plic_reg_top.sv
@@ -4497,6 +4497,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/rv_timer/dv/tb/rv_timer_bind.sv b/hw/ip/rv_timer/dv/tb/rv_timer_bind.sv index a977922..684e066 100644 --- a/hw/ip/rv_timer/dv/tb/rv_timer_bind.sv +++ b/hw/ip/rv_timer/dv/tb/rv_timer_bind.sv
@@ -4,7 +4,9 @@ module rv_timer_bind; - bind rv_timer tlul_assert tlul_assert_host ( + bind rv_timer tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i),
diff --git a/hw/ip/rv_timer/dv/tb/tb.sv b/hw/ip/rv_timer/dv/tb/tb.sv index 004154d..c70ccd1 100644 --- a/hw/ip/rv_timer/dv/tb/tb.sv +++ b/hw/ip/rv_timer/dv/tb/tb.sv
@@ -47,8 +47,8 @@ uvm_config_db#(intr_vif)::set(null, "*.env", "intr_vif", intr_if); uvm_config_db#(alerts_vif)::set(null, "*.env", "alerts_vif", alerts_if); uvm_config_db#(devmode_vif)::set(null, "*.env", "devmode_vif", devmode_if); - uvm_config_db#(tlul_assert_vif)::set(null, "*.env", "tlul_assert_vif", - tb.dut.tlul_assert_host); + uvm_config_db#(tlul_assert_ctrl_vif)::set(null, "*.env", "tlul_assert_ctrl_vif", + dut.tlul_assert_device.tlul_assert_ctrl_if); uvm_config_db#(virtual tl_if)::set(null, "*.env.m_tl_agent*", "vif", tl_if); $timeformat(-12, 0, " ps", 12); run_test();
diff --git a/hw/ip/rv_timer/rtl/rv_timer_reg_top.sv b/hw/ip/rv_timer/rtl/rv_timer_reg_top.sv index 4e88418..b0633c0 100644 --- a/hw/ip/rv_timer/rtl/rv_timer_reg_top.sv +++ b/hw/ip/rv_timer/rtl/rv_timer_reg_top.sv
@@ -484,6 +484,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/spi_device/dv/tb/spi_device_bind.sv b/hw/ip/spi_device/dv/tb/spi_device_bind.sv index 95bb937..3cddf0a 100644 --- a/hw/ip/spi_device/dv/tb/spi_device_bind.sv +++ b/hw/ip/spi_device/dv/tb/spi_device_bind.sv
@@ -4,7 +4,9 @@ module spi_device_bind; - bind spi_device tlul_assert tlul_assert_host ( + bind spi_device tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i),
diff --git a/hw/ip/spi_device/dv/tb/tb.sv b/hw/ip/spi_device/dv/tb/tb.sv index 6514605..f093f66 100644 --- a/hw/ip/spi_device/dv/tb/tb.sv +++ b/hw/ip/spi_device/dv/tb/tb.sv
@@ -76,8 +76,8 @@ uvm_config_db#(intr_vif)::set(null, "*.env", "intr_vif", intr_if); uvm_config_db#(alerts_vif)::set(null, "*.env", "alerts_vif", alerts_if); uvm_config_db#(devmode_vif)::set(null, "*.env", "devmode_vif", devmode_if); - uvm_config_db#(tlul_assert_vif)::set(null, "*.env", "tlul_assert_vif", - tb.dut.tlul_assert_host); + uvm_config_db#(tlul_assert_ctrl_vif)::set(null, "*.env", "tlul_assert_ctrl_vif", + dut.tlul_assert_device.tlul_assert_ctrl_if); uvm_config_db#(virtual tl_if)::set(null, "*.env.m_tl_agent*", "vif", tl_if); uvm_config_db#(virtual spi_if)::set(null, "*.env.m_spi_agent*", "vif", spi_if); $timeformat(-12, 0, " ps", 12);
diff --git a/hw/ip/spi_device/rtl/spi_device_reg_top.sv b/hw/ip/spi_device/rtl/spi_device_reg_top.sv index 565be51..f7f1893 100644 --- a/hw/ip/spi_device/rtl/spi_device_reg_top.sv +++ b/hw/ip/spi_device/rtl/spi_device_reg_top.sv
@@ -1532,6 +1532,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/tlul/common.core b/hw/ip/tlul/common.core index 1ef2417..9604a40 100644 --- a/hw/ip/tlul/common.core +++ b/hw/ip/tlul/common.core
@@ -8,6 +8,7 @@ filesets: files_rtl: depend: + - lowrisc:dv:pins_if - lowrisc:prim:all - lowrisc:tlul:headers files:
diff --git a/hw/ip/tlul/doc/TlulProtocolChecker.md b/hw/ip/tlul/doc/TlulProtocolChecker.md index 73fc72f..9069af4 100644 --- a/hw/ip/tlul/doc/TlulProtocolChecker.md +++ b/hw/ip/tlul/doc/TlulProtocolChecker.md
@@ -33,10 +33,18 @@ defines the structs for channels A and D. * In below tables, "known" means that a signal should have a value other than X. +* The protocol checker has a parameter `EndpointType` which can either be +`"Host"` or `"Device"`. The difference between the `"Host"` and `"Device"` +variant is that some of the properties are formulated as SV assumptions in the +former, whereas the same properties are formulated as SV assertions in the +latter (and vice versa). The behavior of these two checkers in DV simulations +is identical, but in formal verification, this distinction is needed (otherwise +some of the assertions would have to be disabled). ## **Request Channel (Channel A)** Below table lists all channel A signals and their checks. +In `"Device"` mode some of these properties are assumptions (`_M` suffix) and in `"Host"` mode they are assertions (`_A` suffix). <table> <tr> @@ -48,60 +56,60 @@ <tr> <td>a_opcode </td> - <td><strong>legalAOpcode</strong>: Only the following 3 opcodes are legal: + <td><strong>legalAOpcode_[M/A]</strong>: Only the following 3 opcodes are legal: Get, PutFullData, PutPartialData. See spec section 6.2. </td> </tr> <tr> <td>a_param </td> - <td><strong>legalAParam</strong>: This field is reserved, it must be 0. See + <td><strong>legalAParam_[M/A]</strong>: This field is reserved, it must be 0. See spec section 6.2. </td> </tr> <tr> <td>a_size </td> - <td><strong>sizeMatchesMask</strong>: a_size can be calculated from a_mask + <td><strong>sizeMatchesMask_[M/A]</strong>: a_size can be calculated from a_mask as follows: 2<sup>a_size</sup> must equal $countones(a_mask). See spec section 4.6. <p> -<strong>aKnown</strong>: Make sure it's not X when a_valid is high. +<strong>aKnown_A</strong>: Make sure it's not X when a_valid is high. </td> </tr> <tr> <td>a_source </td> - <td><strong>onlyOnePendingReqPerSourceID</strong>: There should be no more + <td><strong>pendingReqPerSrc_[M/A]</strong>: There should be no more than one pending request per each source ID. See spec section 5.4. <p> -<strong>aKnown</strong>: Make sure it's not X when a_valid is high. +<strong>aKnown_A</strong>: Make sure it's not X when a_valid is high. </td> </tr> <tr> <td>a_address </td> - <td><strong>addressAlignedToSize</strong>: a_address must be aligned to + <td><strong>addrSizeAligned_[M/A]</strong>: a_address must be aligned to a_size: a_address & ((1 << a_size) - 1) == 0. See spec section 4.6. <p> -<strong>aKnown: </strong>Make sure it's not X when a_valid is high. +<strong>aKnown_A</strong>Make sure it's not X when a_valid is high. </td> </tr> <tr> <td>a_mask </td> - <td><strong>maskMustBeContiguous</strong>: a_mask must be contiguous for Get + <td><strong>contigMask_[M/A]</strong>: a_mask must be contiguous for Get and PutFullData (but not for PutPartialData). See spec sections 4.6 and 6.2. <p> -<strong>sizeMatchesMask</strong>: See a_size above. +<strong>sizeMatchesMask_[M/A]</strong>: See a_size above. <p> -<strong>aKnown: </strong>Make sure it's not X when a_valid is high. +<strong>aKnown_A</strong>Make sure it's not X when a_valid is high. </td> </tr> <tr> <td>a_data </td> - <td><strong>aDataKnown</strong>: a_data should not be X for opcodes + <td><strong>aDataKnown_[M/A]</strong>: a_data should not be X for opcodes PutFullData and PutPartialData (it can be X for Get). Bytes of a_data, whose corresponding a_mask bits are 0, can be X. See spec section 4.6. </td> @@ -109,19 +117,19 @@ <tr> <td>a_user </td> - <td><strong>aKnown: </strong>Make sure it's not X when a_valid is high. + <td><strong>aKnown_A</strong>Make sure it's not X when a_valid is high. </td> </tr> <tr> <td>a_valid </td> - <td><strong>aKnown</strong>: Make sure it's not X (except during reset). + <td><strong>aKnown_A</strong>: Make sure it's not X (except during reset). </td> </tr> <tr> <td>a_ready </td> - <td><strong>aReadyKnown</strong>: Make sure it's not X (except during + <td><strong>aReadyKnown_A</strong>: Make sure it's not X (except during reset). </td> </tr> @@ -130,6 +138,7 @@ ## **Response Channel (Channel D)** Below table lists all channel D signals and their checks. +In `"Device"` mode some of these properties are assertions (`_A` suffix) and in `"Host"` mode they are assumptions (`_M` suffix). <table> <tr> @@ -141,7 +150,7 @@ <tr> <td>d_opcode </td> - <td><strong>checkResponseOpcode</strong>: If the original request was Get, + <td><strong>respOpcode_[A/M]</strong>: If the original request was Get, then the corresponding response must be AccessAckData. Otherwise, the response must be AccessAck. See spec section 6.2. </td> @@ -149,40 +158,40 @@ <tr> <td>d_param </td> - <td><strong>legalDParam</strong>: This field is reserved, it must be 0. See + <td><strong>legalDParam_[A/M]</strong>: This field is reserved, it must be 0. See spec section 6.2. </td> </tr> <tr> <td>d_size </td> - <td><strong>responseSizeMustEqualReqSize</strong>: The response must have + <td><strong>respSzEqReqSz_[A/M]</strong>: The response must have the same size as the original request. See spec section 6.2. </td> </tr> <tr> <td>d_source </td> - <td><strong>responseMustHaveReq</strong>: For each response, there must have + <td><strong>respMustHaveReq_[A/M]</strong>: For each response, there must have been a corresponding request with the same source ID value. See spec section 5.4. <p> -<strong>noOutstandingReqsAtEndOfSim</strong>: Make sure that there are no +<strong>noOutstandingReqsAtEndOfSim_A</strong>: Make sure that there are no outstanding requests at the end of the simulation. <p> -<strong>dKnown</strong>: Make sure it's not X when d_valid is high. +<strong>dKnown_A</strong>: Make sure it's not X when d_valid is high. </td> </tr> <tr> <td>d_sink </td> - <td><strong>dKnown</strong>: Make sure it's not X when d_valid is high. + <td><strong>dKnown_A</strong>: Make sure it's not X when d_valid is high. </td> </tr> <tr> <td>d_data </td> - <td><strong>dDataKnown</strong>: d_data should not be X for AccessAckData. + <td><strong>dDataKnown_[A/M]</strong>: d_data should not be X for AccessAckData. Bytes of d_data, whose corresponding mask bits of the original request are 0, can be X. See spec section 4.6. </td> @@ -190,25 +199,25 @@ <tr> <td>d_error </td> - <td><strong>dKnown: </strong>Make sure it's not X when d_valid is high. + <td><strong>dKnown_A</strong>Make sure it's not X when d_valid is high. </td> </tr> <tr> <td>d_user </td> - <td><strong>dKnown: </strong>Make sure it's not X when d_valid is high. + <td><strong>dKnown_A</strong>Make sure it's not X when d_valid is high. </td> </tr> <tr> <td>d_valid </td> - <td><strong>dKnown</strong>: Make sure it's not X (except during reset). + <td><strong>dKnown_A</strong>: Make sure it's not X (except during reset). </td> </tr> <tr> <td>d_ready </td> - <td><strong>dReadyKnown: </strong>Make sure it's not X (except during + <td><strong>dReadyKnown_A</strong>Make sure it's not X (except during reset). </td> </tr>
diff --git a/hw/ip/tlul/dv/tb/tlul_adapter_sram_bind.sv b/hw/ip/tlul/dv/tb/tlul_adapter_sram_bind.sv index a372c73..5d73fce 100644 --- a/hw/ip/tlul/dv/tb/tlul_adapter_sram_bind.sv +++ b/hw/ip/tlul/dv/tb/tlul_adapter_sram_bind.sv
@@ -4,7 +4,9 @@ module tlul_adapter_sram_bind; - bind tlul_adapter_sram tlul_assert tlul_assert_host ( + bind tlul_adapter_sram tlul_assert #( + .EndpointType("Device") + ) tlul_assert_host ( .clk_i, .rst_ni, .h2d (tl_i),
diff --git a/hw/ip/tlul/dv/tb/tlul_socket_1n_bind.sv b/hw/ip/tlul/dv/tb/tlul_socket_1n_bind.sv index 3921b7c..14b89b6 100644 --- a/hw/ip/tlul/dv/tb/tlul_socket_1n_bind.sv +++ b/hw/ip/tlul/dv/tb/tlul_socket_1n_bind.sv
@@ -4,14 +4,19 @@ module tlul_socket_1n_bind; - bind tlul_socket_1n tlul_assert tlul_assert_host ( + bind tlul_socket_1n tlul_assert #( + .EndpointType("Host") + ) tlul_assert_host ( .clk_i, .rst_ni, .h2d (tl_h_i), .d2h (tl_h_o) ); - bind tlul_socket_1n tlul_assert_multiple #(N) tlul_assert_device ( + bind tlul_socket_1n tlul_assert_multiple #( + .N(N), + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_d_o),
diff --git a/hw/ip/tlul/dv/tb/tlul_socket_m1_bind.sv b/hw/ip/tlul/dv/tb/tlul_socket_m1_bind.sv index 53a7a20..a2c5eb4 100644 --- a/hw/ip/tlul/dv/tb/tlul_socket_m1_bind.sv +++ b/hw/ip/tlul/dv/tb/tlul_socket_m1_bind.sv
@@ -4,14 +4,19 @@ module tlul_socket_m1_bind; - bind tlul_socket_m1 tlul_assert_multiple #(M) tlul_assert_host ( + bind tlul_socket_m1 tlul_assert_multiple #( + .N(M), + .EndpointType("Host") + ) tlul_assert_host ( .clk_i, .rst_ni, .h2d (tl_h_i), .d2h (tl_h_o) ); - bind tlul_socket_m1 tlul_assert tlul_assert_device ( + bind tlul_socket_m1 tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_d_o),
diff --git a/hw/ip/tlul/rtl/tlul_assert.sv b/hw/ip/tlul/rtl/tlul_assert.sv index e99c351..bb418ef 100644 --- a/hw/ip/tlul/rtl/tlul_assert.sv +++ b/hw/ip/tlul/rtl/tlul_assert.sv
@@ -2,9 +2,12 @@ // Licensed under the Apache License, Version 2.0, see LICENSE for details. // SPDX-License-Identifier: Apache-2.0 -// Protocol checker for TL-UL ports using assertions +// Protocol checker for TL-UL ports using assertions. Supports interface-widths +// up to 64bit. -interface tlul_assert ( +module tlul_assert #( + parameter EndpointType = "Device" // can be either "Host" or "Device" +) ( input clk_i, input rst_ni, @@ -13,6 +16,8 @@ input tlul_pkg::tl_d2h_t d2h ); +`ifndef VERILATOR + import tlul_pkg::*; import top_pkg::*; @@ -35,92 +40,43 @@ pend_req_t [2**TL_AIW-1:0] pend_req; + // this interfaces allows the testbench to disable some assertions + // by driving the corresponding pin to 1'b0 + wire tlul_assert_ctrl, disable_sva; + pins_if #(1) tlul_assert_ctrl_if(tlul_assert_ctrl); + // the interface may be uninitialized, in which case the assertions + // shall be enabled, hence the explicit check for 1'b0 + assign disable_sva = (tlul_assert_ctrl === 1'b0); + + logic [7:0] a_mask, d_mask; + logic [63:0] a_data, d_data; + assign a_mask = 8'(h2d.a_mask); + assign a_data = 64'(h2d.a_data); + assign d_mask = 8'(pend_req[d2h.d_source].mask); + assign d_data = 64'(d2h.d_data); + + //////////////////////////////////// + // keep track of pending requests // + //////////////////////////////////// + // use negedge clk to avoid possible race conditions always_ff @(negedge clk_i or negedge rst_ni) begin if (!rst_ni) begin - for (int ii = 0; ii < 2**TL_AIW; ii++) begin - pend_req[ii].pend = 0; - end + pend_req = '0; end else begin - - - //////////////////// - // check requests // - //////////////////// if (h2d.a_valid) begin - - // a_opcode: only 3 opcodes are legal for requests - `ASSERT_I(legalAOpcode, (h2d.a_opcode === PutFullData) || (h2d.a_opcode === Get) - || (h2d.a_opcode === PutPartialData)) - - // a_param is reserved - `ASSERT_I(legalAParam, h2d.a_param === '0) - - // a_size: Size shouldn't be greater than the bus width in TL-UL (not in TL-UH) - // This assertion can be covered by below - // (a_size must less than or equal to ones of a_mask) - - // a_size: 2**a_size must greater than or equal to $countones(a_mask) for PutPartial and Get - `ASSERT_I(sizeGTEMask, (h2d.a_opcode == PutFullData) || - ((1 << h2d.a_size) >= $countones(h2d.a_mask))) - - // a_size: 2**a_size must equal to $countones(a_mask) for PutFull - `ASSERT_I(sizeMatchesMask, (h2d.a_opcode inside {PutPartialData, Get}) || - ((1 << h2d.a_size) === $countones(h2d.a_mask))) - - // a_source: there should be no more than one pending request per each source ID - `ASSERT_I(onlyOnePendingReqPerSourceID, pend_req[h2d.a_source].pend == 0) - - // a_address must be aligned to a_size: a_address & ((1 << a_size) - 1) == 0 - `ASSERT_I(addressAlignedToSize, (h2d.a_address & ((1 << h2d.a_size)-1)) == '0) - - // a_mask must be contiguous for Get and PutFullData requests - // TODO: the spec talks about "naturally aligned". Does this mean that bit [0] of - // mask is always 1? If that's true, then below code could be much simpler. - // However, the spec shows a timing diagram where bit 0 of mask is 0. - if (h2d.a_opcode != PutPartialData) begin - `ASSERT_I(maskMustBeContiguous, $countones(h2d.a_mask ^ - {h2d.a_mask[$bits(h2d.a_mask)-2:0], 1'b0}) <= 2) - end - - // TODO: a_mask in innactive lanes should be LOW - - // a_data must be known for opcode == Put*(depending on mask bits) - for (int ii = 0; ii < TL_DBW; ii++) begin - if (h2d.a_mask[ii] && (h2d.a_opcode != Get)) begin - `ASSERT_I(aDataKnown, !$isunknown(h2d.a_data[8*ii +: 8])) - end - end - // store each request in pend_req array (we use blocking statements below so // that we can handle the case where request and response for the same // source-ID happen in the same cycle) if (d2h.a_ready) begin - pend_req[h2d.a_source].pend = 1; - pend_req[h2d.a_source].opcode = h2d.a_opcode; - pend_req[h2d.a_source].size = h2d.a_size; - pend_req[h2d.a_source].mask = h2d.a_mask; + pend_req[h2d.a_source].pend = 1; + pend_req[h2d.a_source].opcode = h2d.a_opcode; + pend_req[h2d.a_source].size = h2d.a_size; + pend_req[h2d.a_source].mask = h2d.a_mask; end end // h2d.a_valid - ///////////////////// - // check responses // - ///////////////////// if (d2h.d_valid) begin - - // d_opcode: if request was Get, then response must be AccessAckData - `ASSERT_I(checkResponseOpcode, d2h.d_opcode === - ((pend_req[d2h.d_source].opcode == Get) ? AccessAckData : AccessAck)) - - // d_param is reserved - `ASSERT_I(legalDParam, d2h.d_param === '0) - - // d_size must equal the a_size of the corresponding request - `ASSERT_I(responseSizeMustEqualReqSize, d2h.d_size === pend_req[d2h.d_source].size) - - // d_source: each response should have a pending request using same source ID - `ASSERT_I(responseMustHaveReq, pend_req[d2h.d_source].pend) - // update pend_req array if (h2d.d_ready) begin pend_req[d2h.d_source].pend = 0; @@ -129,17 +85,184 @@ end end - // d_data must be known for AccessAckData (depending on mask bits) - for (genvar ii = 0; ii < TL_DBW; ii++) begin : gen_assert_d_data_known - `ASSERT(dDataKnown, - d2h.d_valid && pend_req[d2h.d_source].mask[ii] && (d2h.d_opcode == AccessAckData) |-> - !$isunknown(d2h.d_data[8*ii +: 8]), - clk_i, !rst_ni) + ///////////////////////////////////////// + // define sequences for request checks // + ///////////////////////////////////////// + + sequence h2d_pre_S; + h2d.a_valid; + endsequence + + // a_opcode: only 3 opcodes are legal for requests + sequence legalAOpcode_S; + (h2d.a_opcode === PutFullData) || + (h2d.a_opcode === Get) || + (h2d.a_opcode === PutPartialData); + endsequence + + // a_param is reserved + sequence legalAParam_S; + h2d.a_param === '0; + endsequence + + // a_size: Size shouldn't be greater than the bus width in TL-UL (not in TL-UH) + // This assertion can be covered by below + // (a_size must less than or equal to ones of a_mask) + + // a_size: 2**a_size must greater than or equal to $countones(a_mask) for PutPartial and Get + sequence sizeGTEMask_S; + (h2d.a_opcode == PutFullData) || ((1 << h2d.a_size) >= $countones(h2d.a_mask)); + endsequence + + // a_size: 2**a_size must equal to $countones(a_mask) for PutFull + sequence sizeMatchesMask_S; + (h2d.a_opcode inside {PutPartialData, Get}) || + ((1 << h2d.a_size) === $countones(h2d.a_mask)); + endsequence + + // a_source: there should be no more than one pending request per each source ID + sequence pendingReqPerSrc_S; + pend_req[h2d.a_source].pend == 0; + endsequence + + // a_address must be aligned to a_size: a_address & ((1 << a_size) - 1) == 0 + sequence addrSizeAligned_S; + (h2d.a_address & ((1 << h2d.a_size)-1)) == '0; + endsequence + + // a_mask must be contiguous for Get and PutFullData requests + // TODO: the spec talks about "naturally aligned". Does this mean that bit [0] of + // mask is always 1? If that's true, then below code could be much simpler. + // However, the spec shows a timing diagram where bit 0 of mask is 0. + sequence contigMask_pre_S; + h2d.a_opcode != PutPartialData; + endsequence + + sequence contigMask_S; + $countones(h2d.a_mask ^ {h2d.a_mask[$bits(h2d.a_mask)-2:0], 1'b0}) <= 2; + endsequence + + // TODO: a_mask in innactive lanes should be LOW + + // a_data must be known for opcode == Put*(depending on mask bits) + sequence aDataKnown_pre_S; + (h2d.a_opcode != Get); + endsequence + + sequence aDataKnown_S; + // no check if this lane mask is inactive + ((!a_mask[0]) || (a_mask[0] && !$isunknown(a_data[8*0 +: 8]))) && + ((!a_mask[1]) || (a_mask[1] && !$isunknown(a_data[8*1 +: 8]))) && + ((!a_mask[2]) || (a_mask[2] && !$isunknown(a_data[8*2 +: 8]))) && + ((!a_mask[3]) || (a_mask[3] && !$isunknown(a_data[8*3 +: 8]))) && + ((!a_mask[4]) || (a_mask[4] && !$isunknown(a_data[8*4 +: 8]))) && + ((!a_mask[5]) || (a_mask[5] && !$isunknown(a_data[8*5 +: 8]))) && + ((!a_mask[6]) || (a_mask[6] && !$isunknown(a_data[8*6 +: 8]))) && + ((!a_mask[7]) || (a_mask[7] && !$isunknown(a_data[8*7 +: 8]))); + endsequence + + ///////////////////////////////////////// + // define sequences for request checks // + ///////////////////////////////////////// + + sequence d2h_pre_S; + d2h.d_valid; + endsequence + + // d_opcode: if request was Get, then response must be AccessAckData + sequence respOpcode_S; + d2h.d_opcode === ((pend_req[d2h.d_source].opcode == Get) ? AccessAckData : AccessAck); + endsequence + + // d_param is reserved + sequence legalDParam_S; + d2h.d_param === '0; + endsequence + + // d_size must equal the a_size of the corresponding request + sequence respSzEqReqSz_S; + d2h.d_size === pend_req[d2h.d_source].size; + endsequence + + // d_source: each response should have a pending request using same source ID + sequence respMustHaveReq_S; + pend_req[d2h.d_source].pend; + endsequence + +// d_data must be known for AccessAckData (depending on mask bits) + sequence dDataKnown_pre_S; + d2h.d_opcode == AccessAckData; + endsequence + + sequence dDataKnown_S; + // no check if this lane mask is inactive + ((!d_mask[0]) || (d_mask[0] && !$isunknown(d_data[8*0 +: 8]))) && + ((!d_mask[1]) || (d_mask[1] && !$isunknown(d_data[8*1 +: 8]))) && + ((!d_mask[2]) || (d_mask[2] && !$isunknown(d_data[8*2 +: 8]))) && + ((!d_mask[3]) || (d_mask[3] && !$isunknown(d_data[8*3 +: 8]))) && + ((!d_mask[4]) || (d_mask[4] && !$isunknown(d_data[8*4 +: 8]))) && + ((!d_mask[5]) || (d_mask[5] && !$isunknown(d_data[8*5 +: 8]))) && + ((!d_mask[6]) || (d_mask[6] && !$isunknown(d_data[8*6 +: 8]))) && + ((!d_mask[7]) || (d_mask[7] && !$isunknown(d_data[8*7 +: 8]))); + endsequence + + /////////////////////////////////// + // assemble properties and check // + /////////////////////////////////// + + // note: use negedge clk to avoid possible race conditions + // in this case all signals coming from the device side have an assumed property + if (EndpointType == "Host") begin : gen_host + // h2d + `ASSERT(legalAOpcode_A, h2d_pre_S |-> legalAOpcode_S, !clk_i, !rst_ni || disable_sva) + `ASSERT(legalAParam_A, h2d_pre_S |-> legalAParam_S, !clk_i, !rst_ni) + `ASSERT(sizeGTEMask_A, h2d_pre_S |-> sizeGTEMask_S, !clk_i, !rst_ni || disable_sva) + `ASSERT(sizeMatchesMask_A, h2d_pre_S |-> sizeMatchesMask_S, !clk_i, !rst_ni || disable_sva) + `ASSERT(pendingReqPerSrc_A, h2d_pre_S |-> pendingReqPerSrc_S, !clk_i, !rst_ni) + `ASSERT(addrSizeAligned_A, h2d_pre_S |-> addrSizeAligned_S, !clk_i, !rst_ni || disable_sva) + `ASSERT(contigMask_A, h2d_pre_S and contigMask_pre_S |-> contigMask_S, + !clk_i, !rst_ni || disable_sva) + `ASSERT(aDataKnown_A, h2d_pre_S and aDataKnown_pre_S |-> aDataKnown_S, !clk_i, !rst_ni) + // d2h + `ASSUME(respOpcode_M, d2h_pre_S |-> respOpcode_S, !clk_i, !rst_ni) + `ASSUME(legalDParam_M, d2h_pre_S |-> legalDParam_S, !clk_i, !rst_ni) + `ASSUME(respSzEqReqSz_M, d2h_pre_S |-> respSzEqReqSz_S, !clk_i, !rst_ni) + `ASSUME(respMustHaveReq_M, d2h_pre_S |-> respMustHaveReq_S, !clk_i, !rst_ni) + `ASSUME(dDataKnown_M, d2h_pre_S and dDataKnown_pre_S |-> dDataKnown_S, + !clk_i, !rst_ni || disable_sva) + // in this case all signals coming from the host side have an assumed property + end else if (EndpointType == "Device") begin : gen_device + // h2d + `ASSUME(legalAOpcode_M, h2d_pre_S |-> legalAOpcode_S, !clk_i, !rst_ni || disable_sva) + `ASSUME(legalAParam_M, h2d_pre_S |-> legalAParam_S, !clk_i, !rst_ni) + `ASSUME(sizeGTEMask_M, h2d_pre_S |-> sizeGTEMask_S, !clk_i, !rst_ni || disable_sva) + `ASSUME(sizeMatchesMask_M, h2d_pre_S |-> sizeMatchesMask_S, !clk_i, !rst_ni || disable_sva) + `ASSUME(pendingReqPerSrc_M, h2d_pre_S |-> pendingReqPerSrc_S, !clk_i, !rst_ni) + `ASSUME(addrSizeAligned_M, h2d_pre_S |-> addrSizeAligned_S, !clk_i, !rst_ni || disable_sva) + `ASSUME(contigMask_M, h2d_pre_S and contigMask_pre_S |-> contigMask_S, + !clk_i, !rst_ni || disable_sva) + `ASSUME(aDataKnown_M, h2d_pre_S and aDataKnown_pre_S |-> aDataKnown_S, !clk_i, !rst_ni) + // d2h + `ASSERT(respOpcode_A, d2h_pre_S |-> respOpcode_S, !clk_i, !rst_ni) + `ASSERT(legalDParam_A, d2h_pre_S |-> legalDParam_S, !clk_i, !rst_ni) + `ASSERT(respSzEqReqSz_A, d2h_pre_S |-> respSzEqReqSz_S, !clk_i, !rst_ni) + `ASSERT(respMustHaveReq_A, d2h_pre_S |-> respMustHaveReq_S, !clk_i, !rst_ni) + `ASSERT(dDataKnown_A, d2h_pre_S and dDataKnown_pre_S |-> dDataKnown_S, + !clk_i, !rst_ni || disable_sva) + end else begin : gen_unknown + initial begin : p_unknonw + `ASSERT_I(unknownConfig_A, 0 == 1) + end + end + + initial begin : p_dbw + // widths up to 64bit / 8 Byte are supported + `ASSERT_I(TlDbw_A, TL_DBW <= 8); end // make sure all "pending" bits are 0 at the end of the sim for (genvar ii = 0; ii < 2**TL_AIW; ii++) begin : gen_assert_final - `ASSERT_FINAL(noOutstandingReqsAtEndOfSim, (pend_req[ii].pend == 0)) + `ASSERT_FINAL(noOutstandingReqsAtEndOfSim_A, (pend_req[ii].pend == 0)) end //////////////////////////////////// @@ -148,70 +271,16 @@ // a_* should be known when a_valid == 1 (a_opcode and a_param are already covered above) // This also covers ASSERT_KNOWN of a_valid - `ASSERT_VALID_DATA(aKnown, h2d.a_valid, {h2d.a_size, h2d.a_source, h2d.a_address, + `ASSERT_VALID_DATA(aKnown_A, h2d.a_valid, {h2d.a_size, h2d.a_source, h2d.a_address, h2d.a_mask, h2d.a_user}, clk_i, !rst_ni) // d_* should be known when d_valid == 1 (d_opcode, d_param, d_size already covered above) // This also covers ASSERT_KNOWN of d_valid - `ASSERT_VALID_DATA(dKnown, d2h.d_valid, {d2h.d_source, d2h.d_sink, d2h.d_error, d2h.d_user}, + `ASSERT_VALID_DATA(dKnown_A, d2h.d_valid, {d2h.d_source, d2h.d_sink, d2h.d_error, d2h.d_user}, clk_i, !rst_ni) // make sure ready is not X after reset - `ASSERT_KNOWN(aReadyKnown, d2h.a_ready, clk_i, !rst_ni) - `ASSERT_KNOWN(dReadyKnown, h2d.d_ready, clk_i, !rst_ni) - -`ifndef VERILATOR - // create functions to enable or disable assertions - `define create_sva_ctrl_function(sva_name_) \ - function void enable_sva_``sva_name_``(); \ - $asserton(1, sva_name_); \ - endfunction \ - \ - function void disable_sva_``sva_name_``(); \ - $assertoff(1, sva_name_); \ - endfunction - - `create_sva_ctrl_function(legalAOpcode) - `create_sva_ctrl_function(sizeMatchesMask) - `create_sva_ctrl_function(addressAlignedToSize) - `create_sva_ctrl_function(maskMustBeContiguous) - `create_sva_ctrl_function(sizeGTEMask) - `create_sva_ctrl_function(dKnownKnownData) - - `undef create_sva_ctrl_function - - function void enable_sva_d_data_known(); - // TODO, for loop, generate block isn't allowed - $asserton(1, gen_assert_d_data_known[0].dDataKnown); - $asserton(1, gen_assert_d_data_known[1].dDataKnown); - $asserton(1, gen_assert_d_data_known[2].dDataKnown); - $asserton(1, gen_assert_d_data_known[3].dDataKnown); - endfunction - - function void disable_sva_d_data_known(); - $assertoff(1, gen_assert_d_data_known[0].dDataKnown); - $assertoff(1, gen_assert_d_data_known[1].dDataKnown); - $assertoff(1, gen_assert_d_data_known[2].dDataKnown); - $assertoff(1, gen_assert_d_data_known[3].dDataKnown); - endfunction - - function void enable_sva_for_tl_errors(); - enable_sva_legalAOpcode(); - enable_sva_sizeMatchesMask(); - enable_sva_addressAlignedToSize(); - enable_sva_maskMustBeContiguous(); - enable_sva_sizeGTEMask(); - enable_sva_d_data_known(); - endfunction - - function void disable_sva_for_tl_errors(); - disable_sva_legalAOpcode(); - disable_sva_sizeMatchesMask(); - disable_sva_addressAlignedToSize(); - disable_sva_maskMustBeContiguous(); - disable_sva_sizeGTEMask(); - disable_sva_d_data_known(); - endfunction + `ASSERT_KNOWN(aReadyKnown_A, d2h.a_ready, clk_i, !rst_ni) + `ASSERT_KNOWN(dReadyKnown_A, h2d.d_ready, clk_i, !rst_ni) `endif -endinterface - +endmodule : tlul_assert
diff --git a/hw/ip/tlul/rtl/tlul_assert_multiple.sv b/hw/ip/tlul/rtl/tlul_assert_multiple.sv index 34dd802..aed5e97 100644 --- a/hw/ip/tlul/rtl/tlul_assert_multiple.sv +++ b/hw/ip/tlul/rtl/tlul_assert_multiple.sv
@@ -5,7 +5,8 @@ // Protocol checker for multiple TL-UL ports module tlul_assert_multiple #( - parameter N = 2 + parameter N = 2, + parameter EndpointType = "Device" // can be "Device" or "Host" ) ( input clk_i, input rst_ni, @@ -17,7 +18,9 @@ // instantiate N tlul_assert modules for (genvar ii = 0; ii < N; ii++) begin : gen_assert - tlul_assert tlul_assert ( + tlul_assert #( + .EndpointType(EndpointType) + ) tlul_assert ( .clk_i, .rst_ni, // TL-UL ports
diff --git a/hw/ip/trial1/rtl/trial1_reg_top.sv b/hw/ip/trial1/rtl/trial1_reg_top.sv index d1d0aba..5de2e1b 100644 --- a/hw/ip/trial1/rtl/trial1_reg_top.sv +++ b/hw/ip/trial1/rtl/trial1_reg_top.sv
@@ -1338,6 +1338,6 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/uart/dv/tb/tb.sv b/hw/ip/uart/dv/tb/tb.sv index 0831894..d984a01 100644 --- a/hw/ip/uart/dv/tb/tb.sv +++ b/hw/ip/uart/dv/tb/tb.sv
@@ -73,8 +73,8 @@ uvm_config_db#(intr_vif)::set(null, "*.env", "intr_vif", intr_if); uvm_config_db#(alerts_vif)::set(null, "*.env", "alerts_vif", alerts_if); uvm_config_db#(devmode_vif)::set(null, "*.env", "devmode_vif", devmode_if); - uvm_config_db#(tlul_assert_vif)::set(null, "*.env", "tlul_assert_vif", - tb.dut.tlul_assert_host); + uvm_config_db#(tlul_assert_ctrl_vif)::set(null, "*.env", "tlul_assert_ctrl_vif", + dut.tlul_assert_device.tlul_assert_ctrl_if); uvm_config_db#(virtual tl_if)::set(null, "*.env.m_tl_agent*", "vif", tl_if); uvm_config_db#(virtual uart_if)::set(null, "*.env.m_uart_agent*", "vif", uart_if); $timeformat(-12, 0, " ps", 12);
diff --git a/hw/ip/uart/dv/tb/uart_bind.sv b/hw/ip/uart/dv/tb/uart_bind.sv index 084654b..e233e33 100644 --- a/hw/ip/uart/dv/tb/uart_bind.sv +++ b/hw/ip/uart/dv/tb/uart_bind.sv
@@ -4,7 +4,9 @@ module uart_bind; - bind uart tlul_assert tlul_assert_host ( + bind uart tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i),
diff --git a/hw/ip/uart/rtl/uart_reg_top.sv b/hw/ip/uart/rtl/uart_reg_top.sv index 7ff1678..fc8edd3 100644 --- a/hw/ip/uart/rtl/uart_reg_top.sv +++ b/hw/ip/uart/rtl/uart_reg_top.sv
@@ -1668,6 +1668,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/usbdev/dv/tb/usbdev_bind.sv b/hw/ip/usbdev/dv/tb/usbdev_bind.sv index e964951..a3c70cc 100644 --- a/hw/ip/usbdev/dv/tb/usbdev_bind.sv +++ b/hw/ip/usbdev/dv/tb/usbdev_bind.sv
@@ -4,7 +4,9 @@ module usbdev_bind; - bind usbdev tlul_assert tlul_assert_host ( + bind usbdev tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_d_i),
diff --git a/hw/ip/usbdev/rtl/usbdev_reg_top.sv b/hw/ip/usbdev/rtl/usbdev_reg_top.sv index fd1a15f..ae50d0f 100644 --- a/hw/ip/usbdev/rtl/usbdev_reg_top.sv +++ b/hw/ip/usbdev/rtl/usbdev_reg_top.sv
@@ -4746,6 +4746,6 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) endmodule
diff --git a/hw/ip/usbuart/dv/tb/usbuart_bind.sv b/hw/ip/usbuart/dv/tb/usbuart_bind.sv index db08694..3d38796 100644 --- a/hw/ip/usbuart/dv/tb/usbuart_bind.sv +++ b/hw/ip/usbuart/dv/tb/usbuart_bind.sv
@@ -4,7 +4,9 @@ module usbuart_bind; - bind usbuart tlul_assert tlul_assert_host ( + bind usbuart tlul_assert #( + .EndpointType("Device") + ) tlul_assert_device ( .clk_i, .rst_ni, .h2d (tl_i),
diff --git a/hw/ip/usbuart/rtl/usbuart_reg_top.sv b/hw/ip/usbuart/rtl/usbuart_reg_top.sv index e93af0b..2167e03 100644 --- a/hw/ip/usbuart/rtl/usbuart_reg_top.sv +++ b/hw/ip/usbuart/rtl/usbuart_reg_top.sv
@@ -1806,6 +1806,8 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule
diff --git a/hw/top_earlgrey/ip/rv_plic/rtl/autogen/rv_plic_reg_top.sv b/hw/top_earlgrey/ip/rv_plic/rtl/autogen/rv_plic_reg_top.sv index 3acc22a..9082f1a 100644 --- a/hw/top_earlgrey/ip/rv_plic/rtl/autogen/rv_plic_reg_top.sv +++ b/hw/top_earlgrey/ip/rv_plic/rtl/autogen/rv_plic_reg_top.sv
@@ -7580,6 +7580,6 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + `ASSUME(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) endmodule
diff --git a/util/reggen/reg_top.sv.tpl b/util/reggen/reg_top.sv.tpl index e5414bb..0cebd04 100644 --- a/util/reggen/reg_top.sv.tpl +++ b/util/reggen/reg_top.sv.tpl
@@ -374,7 +374,9 @@ `ASSERT(en2addrHit, (reg_we || reg_re) |-> $onehot0(addr_hit), clk_i, !rst_ni) - `ASSERT(reqParity, tl_reg_h2d.a_valid |-> tl_reg_h2d.a_user.parity_en == 1'b0, clk_i, !rst_ni) + // 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, clk_i, !rst_ni) endmodule <%def name="str_bits_sv(msb, lsb)">\
diff --git a/util/uvmdvgen/tb.sv.tpl b/util/uvmdvgen/tb.sv.tpl index 9bd5d84..3f46bba 100644 --- a/util/uvmdvgen/tb.sv.tpl +++ b/util/uvmdvgen/tb.sv.tpl
@@ -67,8 +67,8 @@ uvm_config_db#(alerts_vif)::set(null, "*.env", "alerts_vif", alerts_if); % endif uvm_config_db#(devmode_vif)::set(null, "*.env", "devmode_vif", devmode_if); - uvm_config_db#(tlul_assert_vif)::set(null, "*.env", "tlul_assert_vif", - tb.dut.tlul_assert_host); + uvm_config_db#(tlul_assert_ctrl_vif)::set(null, "*.env", "tlul_assert_ctrl_vif", + dut.tlul_assert_device.tlul_assert_ctrl_if); uvm_config_db#(virtual tl_if)::set(null, "*.env.m_tl_agent*", "vif", tl_if); % endif % for agent in env_agents: