Mothers of Pipelines |
| |
Authors: | Sava Krsti , Robert B. Jones,John O'Leary |
| |
Affiliation: | aStrategic CAD Labs, Intel Corporation, Hillsboro, Oregon, USA |
| |
Abstract: | We present a method for pipeline verification using SMT solvers. It is based on a non-deterministic “mother pipeline” machine (MOP) that abstracts the instruction set architecture (ISA). The MOP vs. ISA correctness theorem splits naturally into a large number of simple subgoals. This theorem reduces proving the correctness of a given pipelined implementation of the ISA to verifying that each of its transitions can be modeled as a sequence of MOP state transitions. |
| |
Keywords: | Pipeline verification stuttering simulation confluence SMT solvers |
本文献已被 ScienceDirect 等数据库收录! |
|