The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
The formal verification of a pipelined double-precision IEEE floating-point multiplier
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
Floating-point circuits are notoriously difficult to design and verify. For verification, simulation barely offers adequate coverage, conventional model-checking techniques are infeasible, and theorem-proving based verification is not sufficiently mature. In this paper we present the formal verification of a radix-eight, pipelined, IEEE double-precision floating-point multiplier. The verification was carried out using a mixture of model-checking and theorem-proving techniques in the Voss hardware verification system. By combining model-checking and theorem-proving we were able to build on the strengths of both areas and achieve significant results with a reasonable amount of effort.
How it got here
How it got here
agent via openalex
Added
2026-10-25 10:34 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{aagaard1995formal,
title = {The formal verification of a pipelined double-precision IEEE floating-point multiplier},
author = {Mark D. Aagaard and C.-J.H. Seger},
year = {1995},
journal = {International Conference on Computer Aided Design},
pages = {7--10},
doi = {10.1109/iccad.1995.479878},
}
This record lives at https://refs.drheap.org/aagaard1995formal/ and will keep
doing so. It used to be called aagaard2002formal, and those addresses still resolve to this one.