@phdthesis{26746,
  abstract     = {{Previous research in proof-carrying hardware has established the feasibility and utility of the approach, and provided a concrete solution for employing it for the certification of functional equivalence checking against a specification, but fell short in connecting it to state-of-the-art formal verification insights, methods and tools. Due to the immense complexity of modern circuits, and verification challenges such as the state explosion problem for sequential circuits, this restriction of readily-available verification solutions severely limited the applicability of the approach in wider contexts.

This thesis closes the gap between the PCH approach and current advances in formal hardware verification, provides methods and tools to express and certify a wide range of circuit properties, both functional and non-functional, and presents for the first time prototypes in which circuits that are implemented on actual reconfigurable hardware are verified with PCH methods. Using these results, designers can now apply PCH to establish trust in more complex circuits, by using more diverse properties which they can express using modern, efficient property specification techniques.}},
  author       = {{Wiersema, Tobias}},
  keywords     = {{Proof-Carrying Hardware, Formal Verification, Sequential Circuits, Non-Functional Properties, Functional Properties}},
  pages        = {{293}},
  publisher    = {{Paderborn University}},
  title        = {{{Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware}}},
  year         = {{2021}},
}