Pipelined circuits operate as an assembly line that starts processing new instructions while older ones
continue execution. Control properties specify the correct behaviour of the pipeline with respect to
how it handles the concurrency between instructions. Control properties stand out as one of the most
challenging aspects of pipelined circuit verification. Their verification depends on the datapath and
memories, which in practice account for the largest part of the state space of the circuit. To alleviate
the state explosion problem, abstraction of memories and datapath becomes mandatory. This thesis
provides a methodology for an efficient abstraction of the datapath under all possible control-visible
behaviours. For verification of control properties, the abstracted datapath is then substituted in place
of the original one and the control circuitry is left unchanged. With respect to control properties, the
abstraction is shown conservative by both language containment and simulation.
For verification of control properties, the pipeline datapath is represented by a network of registers,
unrestricted combinational datapath blocks and muxes. The values flowing through the datapath are
called parcels. The control is the state machine that steers the parcels through the network. As parcels
travel through the pipeline, they undergo transformations through the datapath blocks. The control-
visible results of these transformations fan-out into control variables which in turn influence the next
stage the parcels are transferred to by the control. The semantics of the datapath is formalized as a
labelled transition system called a parcel automaton. Parcel automata capture the set of all control
visible paths through the pipeline and are derived without the need of reachability analysis of the
original pipeline. Datapath abstraction is defined using familiar concepts such as language containment
or simulation. We have proved results that show that datapath abstraction leads to pipeline abstraction.
Our approach has been incorporated into a practical algorithm that yields directly the abstract parcel
automaton, bypassing the construction of the concrete parcel automaton. The algorithm uses a SAT
solver to generate incrementally all possible control visible behaviours of the pipeline datapath. Our
largest case study is a 32-bit two-wide superscalar OpenRISC microprocessor written in VHDL, where
it reduced the size of the implementation from 35k gates to 2k gates in less than 10 minutes while using
less than 52MB of memory.
| Identifer | oai:union.ndltd.org:WATERLOO/oai:uwspace.uwaterloo.ca:10012/5804 |
| Date | 18 February 2011 |
| Creators | Vlad, Ciubotariu |
| Source Sets | University of Waterloo Electronic Theses Repository |
| Language | English |
| Detected Language | English |
| Type | Thesis or Dissertation |
Page generated in 0.0017 seconds