Name
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1016/j.entcs.2006.11.036 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
mop state transition,mother pipeline,smt solvers,pipelined implementation,instruction set architecture,pipeline verification,large number,stuttering simulation,simple subgoals,confluence,state transition | Pipeline transport,Programming language,Computer science,Instruction set,Correctness,Parallel computing,Confluence | Journal |
Volume | Issue | ISSN |
174 | 8 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
2 | 0.38 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sava Krstić | 1 | 144 | 9.41 |
| Robert B. Jones | 2 | 434 | 39.17 |
| John O'Leary | 3 | 14 | 2.11 |