Mechanical certification of loop pipelining transformations: a preview

DOI10.1007/978-3-319-08970-6_37MaRDI QIDQ2879278zbMATH OpenOpenAlexFDO

Authors Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie

Publication date 8 September 2014

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08970-6_37

zbMATH Keywords

behavioral synthesiselectronic system level designequivalence checkingtheorem proving

Mathematics Subject Classification ID

Recommendations

• A simple, verified validator for software pipelining
• Formal Methods for Hardware Verification
• scientific article; zbMATH DE number 1507239
• Computer Aided Verification
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant

Cited in

(2)

• Formal verification for high-assurance behavioral synthesis
• Theorem proving guided development of formal assertions in a resource-constrained scheduler for high-level synthesis

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: Mechanical certification of loop pipelining transformations: a preview

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879278)