“Application of Formal Methods (SAT/SMT) to the Design of Constrained Codes” by Sunil Sudhakaran, Clark Barrett, and Mark Horowitz. In Proceedings of Design, Automation & Test in Europe Conference (DATE '25), Apr. 2025. Lyon, France.
Constrained coding plays a crucial role in high-speed communication links by restricting bit sequences to reduce the adverse effects imposed by the characteristics of the channel. This technique trades off some bit efficiency for higher transmission rates, thereby boosting overall data throughput. We show how the design of hardware-efficient translation logic to and from the restricted code space can be formulated as a Satisfiability Modulo Theories (SMT) problem. Using SMT, we can not only try to minimize the complexity of this logic and limit the effect of transmission errors on the final decoded output, but also significantly reduce development time—from weeks to just hours. Our initial results demonstrate the efficiency and effectiveness of this approach.
BibTeX entry:
@inproceedings{SBH25,
author = {Sunil Sudhakaran and Clark Barrett and Mark Horowitz},
title = {Application of Formal Methods {(SAT/SMT)} to the Design of
Constrained Codes},
booktitle = {Proceedings of Design, Automation {&} Test in Europe
Conference (DATE '25)},
publisher = {IEEE},
month = apr,
year = {2025},
doi = {10.23919/DATE64628.2025.10992737},
note = {Lyon, France},
url = {http://theory.stanford.edu/~barrett/pubs/SBH25.pdf}
}
(This webpage was created with bibtex2web.)