Verifying correct pipeline implementation for microprocessors
Jeremy R. Levitt, Kunle Olukotun · International Conference on Computer Aided Design · 1997
We introduce a general, automatic verification technique for pipelined designs. The technique is based on a scalable, formal methodology for analyzing 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.