Verifying correct pipeline implementation for microprocessors

We introduce a general, automatic verification technique for pipelined designs. The technique is based on a scalable, formal methodology for analysing pipelines. The key advantages to our technique are: it specifically targets pipeline control, making it more efficient; it requires no explicit specification, since it compares hardware against itself; it can be used within the broader framework of hierarchical verification; and, it can be easily extended to handle certain "complex" pipelined structures.