Assertion for credit based Design

SystemVerilog
1

SPEC: We have DUT upon POR it will have 100 credits
If it gets 1 REQ as an input,it’s credits will get decreased by 1
If it gets the 10 REQ as an input it’s credits will get decreased by 10
DUT has only one bit ACK, if it is high for 1 clk cycle i.e it acknowledges 1 req and it’s credits will get increased by 1…
similarly, If ACK is high for 10 clk cycle i.e it acknowledges the 10 REQ at one go and credits will get increased by 10
Note : ACK is single bit, where REQ is multi bit

could somebody suggest, if it is possible to write the SV assertion

Thanks in Advance

2

I would start with an automatic task triggered by what starts the process.
The task has the counter and loops and fork-join if needed. Use an immediate assertion at the conclusion.
You should be able to write the code.
Give it a try and give us what you come up with.
SVA will have a problem with local variables being processed by multiple and/or threads.
After the task model I’ll look at the translation into sva

3 
// transaction class
class credit_seq extends uvm_sequence_item 
 rand bit [7:0] request;
 static int credit_count =100;
constraint c1 {request <= credit_count;}
endclass


   // driver class
forever begin
   if (!my_txn.request)
       seq_item_port.get (my_txn);
     vif.request <= my_txn.request; // Send to DUT
     credit_count = credit_count - my_txn.request;
        fork
             begin
                 while (vif.ack) begin
                     @posedge clk;
                     credit_count ++;
                 end
             end
        join_none  
end

Details:
The Driver can send the requests, based on the credits available in the DUT
So started with the assumption that DUT has 100 credits and the driver keeps on sending the requests untill DUT has credits
Driver tracks the credit count by incr/dcr the credit_count value i.e if ack comes then the available credits will get increased…