Solver technology for system-level to RTL equivalence checking
The work
| Authors | Alfred Koelbl; R. Jacoby; Himanshu Jain; Carl Pixley |
|---|---|
| Editors | |
| Type | misc |
| Year | 2009 |
| Citekey | koelbl2009solver |
Where it appeared
| Published in | Design, Automation, and Test in Europe |
|---|---|
| Pages | 196--201 |
Identifiers
| DOI | 10.1109/date.2009.5090657 |
|---|---|
| OpenAlex | W3148913902 |
Access
| Landing page | https://doi.org/10.1109/date.2009.5090657 |
|---|
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
Checking the equivalence of a system-level model against an RTL design is a major challenge. The reason is that usually the system-level model is written by a system architect, whereas the RTL implementation is created by a hardware designer. This approach leads to two models that are significantly different. Checking the equivalence of real-life designs requires strong solver technology. The challenges can only be overcome with a combination of bit-level and word-level reasoning techniques, combined with the right orchestration. In this paper, we discuss solver technology that has shown to be effective on many real-life equivalence checking problems.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 17:17 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{koelbl2009solver,
title = {Solver technology for system-level to RTL equivalence checking},
author = {Alfred Koelbl and R. Jacoby and Himanshu Jain and Carl Pixley},
year = {2009},
journal = {Design, Automation, and Test in Europe},
pages = {196--201},
doi = {10.1109/date.2009.5090657},
}
This record lives at https://refs.drheap.org/koelbl2009solver/ and will keep doing so.