Mothers of Pipelines | Zendy

Sava Krstić | Zendy; Robert B. Jones | Zendy; John O’Leary | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Mothers of Pipelines

Author(s) -

Sava Krstić,

Robert B. Jones,

John O’Leary

Publication year - 2007

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2006.11.036

Subject(s) - correctness , pipeline (software) , computer science , pipeline transport , set (abstract data type) , simple (philosophy) , sequence (biology) , state (computer science) , programming language , theoretical computer science , algorithm , parallel computing , engineering , philosophy , epistemology , environmental engineering , biology , genetics

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research