How to write sv assertion to prove a packet with valid and some txnid in the input inside dut undergoes some translation and come out with same txnid and valid but time between input to output may vary for each request?

SystemVerilog
, , ,
1

HI all

I am trying to prove below scenario in formal but need some help in writing assertion.

DUT spec:

  1. inputs : i_rxvalid , i_rxpkt(txnid, srcid, data etc), i_txcredit

  2. output : o_txvalid , o_txpkt(txnid, data, etc.) , o_rxcredit

  3. After reset credits are sent by DUT on o_rxcedit and paralley received from other side on i_txcredit independently

  4. from rx side say 4 requests have come back to back with txnid - 'h1, 'h2, 'h3, 'h4 on i_rxvalid & i_rxpkt

  5. after some processing these 4 requests would go out of DUT out of order with some random delay between them on o_txvalid & o_txpkt say 'h3, 'h2, 'h1, 'h4 but the max delay between input to output is 500 cycles.

How can we write an assertion property to prove that for each valid request with some txn_id there was valid output with same txn_id?

Thanks

2

In reply to uanthire:

You need support logic. See my paper:
SUPPORT LOGIC AND THE always PROPERTY

Provides examples of support logic needed for certain types of requirements where the strict use of only SVA does not cover

Your requirements are very loosely written.
Read the paper on support logic to help in specifying uniqueness in assertions.
Write code, do a quick TB.
If unclear, come back here and we’ll take a look at the issues.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog