diff --git a/src/frontend/sras.sv b/src/frontend/sras.sv
index 3a97c2e45532b35e9efcc7967a16848efbd080c2..498fddf2a79d9e7326aeb6b6968e37d8d0428637 100644
--- a/src/frontend/sras.sv
+++ b/src/frontend/sras.sv
@@ -95,4 +95,17 @@ module sras #(
             tos_q        <= tos_d;
         end
     end
+
+    // pragma translate_off
+    `ifndef VERILATOR
+      initial begin
+         assert (2 ** $clog2(SpecDepth) == SpecDepth) else $fatal(1,"[sras] SpecDepth is not a power of 2");
+         assert (2 ** $clog2(DEPTH) == DEPTH) else $fatal(1,"[sras] DEPTH is not a power of 2");
+      end
+
+      assert property (
+        @(posedge clk_i) disable iff (!rst_ni) push_i |-> begin_spec_i)
+          else $warning (1,"[sras] push_i & ~begin_spec_i");
+    `endif
+    // pragma translate_on
 endmodule