How do write SVA for sequential req followed by ack ??

This is tricky and generally we get confuse and think that req |-> ##[1:$] ack ; will give the correct result but this is not true

The solution for this issue is

module req_ack_sequential_checker(
input bit clk,
input bit req,
input bit ack
);
bit error_flag ; // Error flag to indicate a protocol violation
bit last_req_acknowledged ; // Flag to check if last request was acknowledged

// Initialize the registers
initial begin
   error_flag <= 0; 
   last_req_acknowledged <=1;  


// Monitor request and acknowledgment signals
forever @(posedge clk) begin
    // Reset error flag each clock cycle for clarity
    //error_flag = 0;

     // Initially true to allow the first request
    if ($rose(req)) begin
        // Check if the last request was acknowledged before accepting a new one

      if (!last_req_acknowledged) begin
            $display("Error: New request issued before the last one was acknowledged.");
            error_flag = 1;  // Set error flag
            $finish;  // Terminate simulation or handle error as needed
        end
        last_req_acknowledged = 0; // A new request has been made, waiting for ack
    end

    if ($rose(ack)) begin
        // Set flag to true when an acknowledgment is received
        last_req_acknowledged = 1;
    end
end
end 

endmodule

Now to give stimulus

`timescale 1ns / 1ps

module tb_req_ack_sequential_checker;
reg clk = 0;
reg req = 0;
reg ack = 0;

// Instantiate the checker module
req_ack_sequential_checker dut(
    .clk(clk),
    .req(req),
    .ack(ack)
);

// Clock generation
always #5 clk = ~clk;  // 100 MHz clock

// Generate test sequence
initial begin
     $dumpfile("req_ack_sequential_checker.vcd");  // Name of the VCD file
    $dumpvars(0, tb_req_ack_sequential_checker);  // Dump all variables of the testbench and submodules

    // Initial state, allow time for initialization
    #10;
    req = 1;  // Issue first request
    #10 req = 0;
    #10 req = 1;  // Issue second request without waiting for ack
    #10 req = 0;
    #10 req = 1;
    #20 ack = 1;  // Acknowledge only the first request after the second one was issued
    #10 ack = 0;
    #40 $stop;  // Stop the simulation after the scenario
end

endmodule

Output :

Log :

ontains Synopsys proprietary information.
Compiler version U-2023.03-SP2_Full64; Runtime version U-2023.03-SP2_Full64; May 7 08:35 2024
Error: New request issued before the last one was acknowledged.
$finish called from file “design.sv”, line 28.