This year at DAC, we asked attendees to participate in a guessing game – make an educated guess about how long it takes to formally verify a design based on the given design description and statistics.
Here is a recap of the information provided to participants:
Reorder IP packets that can arrive out of order and dequeue them in order; when an exception occurs, the design flushes the IP packets for which exceptions has occurred. Support 36 different inputs that can send the data for one or more ports. Another interface provides dequeue requests for different ports. Design supports 48 different ports.
Packets arrive with valid signal; a request/grant mechanism for handling requests from 36 different sources; All 36 inputs are independent and can arrive concurrently; All 48 ports can be dequeued in parallel using another request/grant mechanism.
Design Micro-architecture Details
Supports enqueue and dequeue for IP packets for 362 different input and 48 different ports respectively; 48 different queues used to store IP packets for different ports; A round robin arbiter resolves contention between enqueue requests from different sources for the same port at the same cycle. (more…)