The Prefetcher Index Cell

The transition diagram for the Prefetcher is shown below. The Prefetcher index cell can also be modelled by a predicated Petri net (E-net), and formally specified. The details are omitted.