A Transistor Level Relational Semantics for Electrical Rule Checking by SMT Solving
The work
| Authors | Oussama Oulkaid; Bruno Ferres; Matthieu Moy; Pascal Raymond; Mehdi Khosravian; Ludovic Henrio; Gabriel Radanne |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2024 |
| Citekey | oulkaid2024transistor |
Where it appeared
| Published in | 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE) |
|---|---|
| Publisher | IEEE |
| Pages | 1--6 |
Identifiers
| DOI | 10.23919/date58400.2024.10546537 |
|---|
Access
| Landing page | https://doi.org/10.23919/date58400.2024.10546537 |
|---|
Related
| Contained in | oulkaid2025modeles |
|---|---|
| Distinct from | basin1989verification |
| Distinct from | ferres2023electrical |
| Distinct from | ferres2025survey |
| Distinct from | gordon1983proving |
| Distinct from | joyce1987hardware |
| Distinct from | lewis2026finding |
| Distinct from | oulkaid2026modeling |
From crossref.
Abstract
We present a novel technique for Electrical Rule Checking (ERC) based on formal methods. We define a relational semantics of Integrated Circuits (IC) as a means to model circuits' behavior at transistor-level. We use Z3, a Satisfiability Modulo Theory (SMT) solver, to verify electrical properties on circuits — thanks to the defined semantics. We demonstrate the usability of the approach to detect current leakage due to missing level-shifter on large industrial circuits, and we conduct experiments to study the scalability of the approach.
A copy is held
pdf, 906.7 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-09-15 21:10 UTC |
| Approved by | a person 2026-09-16 09:30 UTC |
Cite it as
@inproceedings{oulkaid2024transistor,
title = {A Transistor Level Relational Semantics for Electrical Rule Checking by SMT Solving},
author = {Oussama Oulkaid and Bruno Ferres and Matthieu Moy and Pascal Raymond and Mehdi Khosravian and Ludovic Henrio and Gabriel Radanne},
year = {2024},
booktitle = {2024 Design, Automation \& Test in Europe Conference \& Exhibition (DATE)},
publisher = {IEEE},
pages = {1--6},
doi = {10.23919/date58400.2024.10546537},
}
This record lives at https://refs.drheap.org/oulkaid2024transistor/ and will keep doing so.