Automatic Hardware Synthesis from Specifications: A Case Study
The work
| Authors | Roderick Bloem; Stefan J. Galler; Barbara Jobstmann; Nir Piterman; Amir Pnueli; Martin Weiglhofer |
|---|---|
| Editors | |
| Type | misc |
| Year | 2007 |
| Citekey | bloem2007automatic |
Where it appeared
| Published in | Design, Automation, and Test in Europe |
|---|---|
| Pages | 1--6 |
Identifiers
| DOI | 10.1109/date.2007.364456 |
|---|---|
| OpenAlex | W2122620434 |
Access
| Landing page | https://doi.org/10.1109/date.2007.364456 |
|---|
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
We propose to use a formal specification language as a high-level hardware description language. Formal languages allow for compact, unambiguous representations and yield designs that are correct by construction. The idea of automatic synthesis from specifications is old, but used to be completely impractical. Recently, great strides towards efficient synthesis from specifications have been made. In this paper we extend these recent methods to generate compact circuits and we show their practicality by synthesizing an arbiter for ARM's AMBA AHB bus and a generalized buffer from specifications given in PSL. These are the first industrial examples that have been synthesized automatically from their specifications
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 02:41 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{bloem2007automatic,
title = {Automatic Hardware Synthesis from Specifications: A Case Study},
author = {Roderick Bloem and Stefan J. Galler and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Martin Weiglhofer},
year = {2007},
journal = {Design, Automation, and Test in Europe},
pages = {1--6},
doi = {10.1109/date.2007.364456},
}
This record lives at https://refs.drheap.org/bloem2007automatic/ and will keep doing so.