From c4da7f0b45f8fb91a2d81df43964832505f4fce8 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Wed, 5 Jan 2022 11:41:48 +0100
Subject: [PATCH] sras: add assertions

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
 src/frontend/sras.sv | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/frontend/sras.sv b/src/frontend/sras.sv
index befa9fb2..053f13ff 100644
--- a/src/frontend/sras.sv
+++ b/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
-- 
GitLab