diff --git a/src/frontend/sras.sv b/src/frontend/sras.sv index befa9fb2891928e8f8f73c69b0152638121db7da..053f13ff62b6de2047a110c92d77bacdb1bc7ee9 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