Revert "cva6: don't backup on direct jumps"

This reverts commit 484754dc.

src/frontend/sras.sv

@@ -67,14 +67,10 @@ module sras #(
                 end else begin
                     if (prev_plus_one == '0 || pp_plus_one == '0) begin
                         ovf_counter_d[ptr_spec_d] = ovf_counter_q[ptr_spec_q] + 1'b1;
-                        if (begin_spec_i) begin
-                            ovf_counter_d[ptr_spec_q] = ovf_counter_q[ptr_spec_q] + 1'b1;
-                        end
+                        ovf_counter_d[ptr_spec_q] = ovf_counter_q[ptr_spec_q] + 1'b1;
                     end else begin
                         tos_d[ptr_spec_d] = prev_plus_one;
-                        if (begin_spec_i) begin
-                            tos_d[ptr_spec_q] = pp_plus_one;
-                        end
+                        tos_d[ptr_spec_q] = pp_plus_one;
                     end
                 end
             end else if (!push_i && pop_i) begin
@@ -121,7 +117,7 @@ module sras #(
     always_comb begin
         prev_stack = stack_q[ptr_spec_q];
 
-        if (can_push && begin_spec_i) begin
+        if (can_push) begin
             prev_stack[pp_plus_one] = to_push;
         end
     end
@@ -157,21 +153,17 @@ 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) (begin_spec_i & !(bad_spec_i)) |-> (ptr_spec_d != ptr_backup_d))
-      //     else $warning (1,"[sras] speculation overflow");
+      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)) |-> (~push_i))
-      //     else $warning (1,"[sras] backup overwrite");
+      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");
+      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