09-05-2013, 03:38 PM
Formal Verification of a System-on-Chip Bus Protocol
Formal Verification.ppt (Size: 144.5 KB / Downloads: 117)
Bus Protocols
Popularity of bus-based SoC designs necessitate the verification of bus protocols.
Different from testing/validating the cores.
SoC Bus Protocols often involve advanced features for high speed data transfer, leading to corner cases
Pipelining
Wait Cycles
Split Transfers
Case study: AMBA AHB protocol from ARM.
Bus architecture
Several masters and slaves are connected to AHB.
An arbiter decides which master will transfer data.
Data is transferred from a master to a slave in bursts.
Any burst involves read/write of a sequence of addresses.
The slave to service a burst is chosen depending on the addresses (decided by a decoder).
AHB is connected to APB via a bus bridge.
Let us study the transfer features of AHB protocol
Split response
Cycle i
Master M drives address A on bus
Cycle i+1
Slave S thinks it can take too long to service A, issues SPLIT response
Arbiter snoops on SPLIT response, records current master.
Issued in (i+1, i+2) to kill already initiated transfers
Cycle i+2
Arbiter disables bus access to current master. Others can now access the bus.
Model Checking
Developed a formal specification of the protocol.
Various kinds of components
> 1 Masters
Slave(s)
Arbiter
Bus interface of each component modeled as a finite state machine.
Protocol = Synchronous composition of these FSMs
Model check temporal properties (e.g. non-starvation) using Cadence SMV tool.
Conclusion
Case study in model checking of a bus protocol with non-trivial data transfer features
Interaction of these features (Pipelining + Splits) leads to a corner case starvation scenario.
Source of starvation was suspected via human understanding of the protocol.
Model checking effort was taken up to:
verify our suspicion.
Find a detailed counter-example trace.