diff --git a/src/frontend/sras.sv b/src/frontend/sras.sv index b1b6b62f83e24f9b912a6bb07246295d929b4df3..4f1aea3ad10cdba17415af8cfebd14ac040abc37 100644 --- a/src/frontend/sras.sv +++ b/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