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