sras: better condition handling (?)

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

src/frontend/sras.sv

@@ -53,21 +53,29 @@ module sras #(
 
         if (flush_i) begin
             tos_d = '0;
-        end else if (push_i && !pop_i) begin
-            tos_d[ptr_spec_d] = prev_plus_one;
-            tos_d[ptr_spec_q] = pp_plus_one;
-        end else if (!push_i && pop_i) begin
-            tos_d[ptr_spec_d] = prev_minus_one;
-        end else if (!bad_spec_i && begin_spec_i) begin
-            tos_d[ptr_spec_d] = tos_q[ptr_spec_q];
+        end else if (!bad_spec_i) begin
+            if (push_i && !pop_i) begin
+                tos_d[ptr_spec_d] = prev_plus_one;
+                if (begin_spec_i) begin
+                    tos_d[ptr_spec_q] = pp_plus_one;
+                end
+            end else if (!push_i && pop_i) begin
+                    tos_d[ptr_spec_d] = prev_minus_one;
+            end else if (begin_spec_i) begin
+                tos_d[ptr_spec_d] = tos_q[ptr_spec_q];
+            end
         end
     end
 
+    logic can_pop, can_push;
+    assign can_pop = pop_i && !bad_spec_i;
+    assign can_push = push_i && !bad_spec_i;
+
     assign data_o = stack_q[previous_tos_addr][previous_tos];
 
     ariane_pkg::ras_t to_push;
     assign to_push.ra = (push_i) ? data_i : 0;
-    assign to_push.valid = push_i;
+    assign to_push.valid = can_push;
 
     ariane_pkg::ras_t [DEPTH-1:0] new_stack, prev_stack;
 
@@ -78,11 +86,9 @@ module sras #(
             new_stack = stack_q[ptr_spec_q];
         end
 
-        if (pop_i) begin
+        if (can_pop) begin
             new_stack[previous_tos] = to_push;
-        end
-
-        if (push_i) begin
+        end else if (can_push) begin
             new_stack[prev_plus_one] = to_push;
         end
     end
@@ -90,7 +96,7 @@ module sras #(
     always_comb begin
         prev_stack = stack_q[ptr_spec_q];
 
-        if (push_i) begin
+        if (can_push && begin_spec_i) begin
             prev_stack[pp_plus_one] = to_push;
         end
     end
@@ -124,9 +130,9 @@ module sras #(
          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) 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))
@@ -135,6 +141,10 @@ module sras #(
       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");
+
+      assert property (
+        @(posedge clk_i) disable iff (!rst_ni) can_push |-> ~can_pop && can_pop |-> ~can_push)
+          else $fatal (1,"[sras] push & pop at the same time");
     `endif
     // pragma translate_on
 endmodule