sras: add assertions

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

src/frontend/sras.sv

@@ -120,12 +120,21 @@ module sras #(
     `ifndef VERILATOR
       initial begin
          assert (2 ** $clog2(SpecDepth) == SpecDepth) else $fatal(1,"[sras] SpecDepth is not a power of 2");
+         assert (SpecDepth >= 2) else $fatal(1,"[sras] SpecDepth is lower than 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");
+
+      assert property (
+        @(posedge clk_i) disable iff (!rst_ni) (begin_spec_i & !(bad_spec_i)) |-> (ptr_spec_d != ptr_backup_d))
+          else $fatal (1,"[sras] speculation overflow");
+
+      assert property (
+        @(posedge clk_i) disable iff (!rst_ni) valid_spec_i |-> ((ptr_backup_q == ptr_spec_q) |-> (ptr_backup_d == ptr_spec_d)))
+          else $fatal (1,"[sras] backup overtake");
     `endif
     // pragma translate_on
 endmodule