Verification of FPGA layout generators in higher-order logic

DOI10.1007/S10817-006-9039-9MaRDI QIDQ877830zbMATH OpenOpenAlexFDO

Authors Oliver Pell

Publication date 3 May 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-006-9039-9

zbMATH Keywords

layout descriptionsroute algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Provably-correct hardware compilation tools based on pass separation techniques
• scientific article; zbMATH DE number 1979560
• scientific article; zbMATH DE number 1400095
• scientific article; zbMATH DE number 139822
• Correct Hardware Design and Verification Methods

Cites work

• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 1979560 (Why is no real title available?)
• scientific article; zbMATH DE number 2084718 (Why is no real title available?)
• scientific article; zbMATH DE number 2102713 (Why is no real title available?)
• A theory of type polymorphism in programming
• Correct Hardware Design and Verification Methods
• Higher Order Logic and Hardware Verification
• Isabelle/HOL. A proof assistant for higher-order logic
• The Principal Type-Scheme of an Object in Combinatory Logic

Cited in

(3)

• Provably-correct hardware compilation tools based on pass separation techniques
• An abstraction algorithm for the verification of level-sensitive latch-based netlists
• scientific article; zbMATH DE number 1979560 (Why is no real title available?)

Describes a project that uses

Uses Software

• Lava
• Xilinx
• Haskell
• CHIP
• Isabelle/HOL
• ML
• Isabelle

This page was built for publication: Verification of FPGA layout generators in higher-order logic

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