A Flexible Formal Verification Framework for Industrial Scale Validation

The work

AuthorsAnna Slobodová; Jared Davis; Sol Swords; Warren A. Hunt, Jr.
Editors
Typeinproceedings
Year2011
Citekeyslobodova2011flexible

Where it appeared

Published in9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2011)
PublisherIEEE
Pages89--97

Related

Distinct frombryant1987algorithmic
Distinct frombryant1991extraction
Distinct frombryant1991memory
Distinct frombryant2021dual
Distinct fromeen2011efficient
Distinct fromjacobi2005automatic
Distinct fromkurze2026nocout
Distinct frommelham1990formalizing
Distinct fromnukala2024translating
Distinct fromoleary2013relational
Distinct fromsaravanan2025synfuzz
Distinct fromzhang2025fastlec

From bibtex.

Abstract

In recent years, leading microprocessor companies have made huge investments to improve the reliability of their products. Besides expanding their validation and CAD tools teams, they have incorporated formal verification methods into their design flows. Formal verification (FV) engineers require extensive training, and FV tools from CAD vendors are expensive. At first glance, it may seem that FV teams are not affordable by smaller companies. We have not found this to be true. This paper describes the formal verification framework we have built on top of publicly-available tools. This framework gives us the flexibility to work on myriad different problems that occur in microprocessor design.

A copy is held

pdf, 183.3 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-09-16 23:43 UTC
Approved bya person 2026-09-23 14:08 UTC

Cite it as

@inproceedings{slobodova2011flexible,
  title        = {A Flexible Formal Verification Framework for Industrial Scale Validation},
  author       = {Anna Slobodová and Jared Davis and Sol Swords and Warren A. Hunt, Jr.},
  year         = {2011},
  booktitle    = {9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2011)},
  publisher    = {IEEE},
  pages        = {89--97},
  doi          = {10.1109/memcod.2011.5970515},
}

This record lives at https://refs.drheap.org/slobodova2011flexible/ and will keep doing so.