2024
- Mertcan Temel "VeSCMul: Verified Implementation of S-C-Rewriting for Multiplier Verification". Proceedings of the 2024 International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024) (to appear)
- Abstract
Formal verification of multipliers is difficult. This paper presents a custom tool, VeSCMul, designed to address this problem. VeSCMul can be effectively applied to a wide range of hardware verification challenges, including multipliers with saturation, flags, shifting, truncation, accumulation, dot product, and even floating-point multiplication. The tool is highly automated with a user-friendly interface, and it is very efficient; for instance, verification for designs with 64-bit operands can finish in seconds. Notably, VeSCMul has been successfully utilized for both commercial designs and publicly available benchmarks. Regarding the reliability of its results, VeSCMul itself is fully verified, instilling confidence in its users for soundness. It also has the option to be used with a SAT solver for completeness and counterexample generation. Readers of this paper will gain insights into the capabilities and limitations of VeSCMul, as well as how to employ it for the verification of their own designs.
- Paper (preprint)
- Bibtex
@InProceedings{Temeltacas24, author="Temel, Mertcan", title = {{VeSCMul}: Verified Implementation of {S-C-Rewriting} for Multiplier Verification}, booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems , {TACAS} 2024 (to appear)}, }
- Abstract
- Mertcan Temel "Formal Verification of Booth Radix-8 and Radix-16 Multipliers". Proceedings of the 2024 Design, Automation & Test in Europe Conference & Exhibition (DATE 2024) (to appear)
- Abstract
In processors where low power consumption is essential, higher Booth encodings such as radix-8 and radix-16 may be preferred over the more common radix-4 encoding. With higher radix multipliers included in commercial hardware, formal verification of such designs poses a real challenge. Verifying multipliers is difficult in general; state-of-the-art verification methods like S-C-Rewriting and computer algebra have primarily addressed the multiplier verification problem for lower Booth radices such as radix-4. However, these methods do not scale well for higher radices. This paper explores the cause of this limitation and proposes a list of solutions for automatic, sound, and fast verification of such designs. These solutions include three improvements for the S-C-Rewriting method, some of which may be applicable to computer algebra methods as well. Experiments have shown that higher Booth radix multipliers can now be verified soundly, fully automatically, and in a matter of seconds for common operand sizes such as 64 and 128 bits.
- Paper (preprint)
- Slides
- Bibtex
@inproceedings{temelDATE2024, year = 2024, author = {Mertcan Temel}, title = {{Formal Verification of Booth Radix-8 and Radix-16 Multipliers}}, booktitle = {Design, Automation {\&} Test in Europe Conference {\&} Exhibition ({DATE}) (to appear)} }
- Abstract
2022
- Mertcan Temel "Verified Implementation of an Efficient Term-Rewriting Algorithm for
Multiplier Verification on ACL2". Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, EPTCS, 2022
- Abstract
Automatic and efficient verification of multiplier designs, especially through a provably correct method, is a difficult problem. We show how to utilize a theorem prover, ACL2, to implement an efficient rewriting algorithm for multiplier design verification. Through a basic understanding of the features and data structures of ACL2, we created a verified program that can automatically verify various multiplier designs much faster than the other state-of-the-art tools. Additionally, users of our system have the flexibility to change the specification for the target design to verify variations of multipliers. We discuss the challenges we tackled during the development of this program as well as key implementation details for efficiency and verifiability. Those who plan to implement an efficient program on a theorem prover or those who wish to implement our multiplier verification methodology on a different system may benefit from the discussions in this paper.
- Paper
- Bibtex
@inproceedings{TemelACL2-2022, author = {Mertcan Temel}, editor = {Rob Sumners and Cuong Chau}, title = {Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on {ACL2}}, booktitle = {Proceedings Seventeenth International Workshop on the {ACL2} Theorem Prover and its Applications, Austin, Texas, USA, 26th-27th May 2022}, series = {{EPTCS}}, volume = {359}, pages = {116--133}, year = {2022}, url = {https://doi.org/10.4204/EPTCS.359.11}, doi = {10.4204/EPTCS.359.11}, timestamp = {Tue, 05 Jul 2022 12:50:48 +0200} }
- Abstract
2021
- Mertcan Temel, Warren A. Hunt "Sound and Automated Verification of Real-World RTL Multipliers". Formal Methods in Computer Aided Design 2021 (FMCAD21), 8 pages, IEEE 2021.
- Abstract
We have developed an algorithm, S-C-Rewriting, that can automatically and very efficiently verify arithmetic modules with embedded multipliers. These include ALUs, dot- product, multiply-accumulate designs that may use Booth en- coding, Wallace-trees, and various vector adders. Outputs of the target multiplier designs might be truncated, right-shifted, or a combination of both. We evaluate the performance of other state-of-the-art tools on verification problems beyond isolated multipliers and we show that our method applies to a broader range of design techniques encountered in real-world modules. Our verification software is verified using the ACL2 theorem prover, and we can soundly verify 1024x1024-bit isolated mul- tipliers and similarly large dot-product designs in minutes. We can also generate counterexamples in case of a design bug. Our tool and benchmarks are available online.
- Paper
- Talk (Video) - Slides (PDF)
- Experiments
- Bibtex
@inproceedings{TemelFmcad21, author = {Mertcan Temel and Warren A. Hunt}, title = {Sound and Automated Verification of Real-World {RTL} Multipliers}, booktitle = {Formal Methods in Computer Aided Design, {FMCAD} 2021, New Haven, CT, USA, October 19-22, 2021}, pages = {53--62}, publisher = {{IEEE}}, year = {2021}, url = {https://doi.org/10.34727/2021/isbn.978-3-85448-046-4\_13}, doi = {10.34727/2021/isbn.978-3-85448-046-4\_13}, timestamp = {Tue, 07 Dec 2021 17:02:16 +0100} }
- Abstract
- Mertcan Temel "Automated, efficient, and sound verification of integer multipliers". University of Texas at Austin, 2021, Dissertation.
- Abstract
Formal verification of multiplier designs has been studied for decades. However, the practicality of the state-of-the-art tools has been limited because they do not scale for large designs or they only support certain types of design methodologies. We have developed a new and widely applicable algorithm, S-C-Rewriting, for efficient and automatic verification of signed and unsigned arithmetic modules with embedded multipliers. The architectures of our target designs include Wallace, Dadda, 4-to-2 compressor trees, and more with Booth encoding and various types of final stage adders. The output of these multipliers may be truncated, right-shifted, or a combination of both, and they may be implemented as part of a multiply-accumulate, dot-product, or other arithmetic units with control logic. Our method and tool are verified using the ACL2 theorem prover, and users can trust the soundness of our verification results. Our experiments have shown that our approach scales well in terms of time and memory. We can soundly confirm the correctness of 1024x1024-bit isolated multiplier and similarly large dot-product designs within a few minutes. Additionally, we can quickly generate counterexamples for flawed designs. Our tool and benchmarks are available online for public use.
- Paper
- Bibtex
@phdthesis{TemelDissertation, title = {Automated, Efficient, and Sound Verification of Integer Multipliers}, school = {The University of Texas at Austin}, author = {Temel, Mertcan}, year = {2021} }
- Abstract
2020
- Mertcan Temel, Anna Slobodova, Warren A. Hunt "Automated and Scalable Verification of Integer Multipliers". Computer Aided Verification 2020 (CAV20), 20 pages, Springer 2020.
- Abstract
The automatic formal verification of multiplier designs has been pursued since the introduction of BDDs. We present a new rewriter-based method for efficient and automatic verification of signed and unsigned integer multiplier designs. We have proved the soundness of this method using the ACL2 theorem prover, and we can verify integer multiplier designs with various architectures automatically, including Wallace, Dadda, and 4-to-2 compressor trees, designed with Booth encoding and various types of final stage adders. Our experiments have shown that our approach scales well in terms of time and memory. With our method, we can confirm the correctness of 1024×1024-bit multiplier designs within minutes.
- Paper
- Preview (Video) - Talk (Video) - Slides (PDF)
- Bibtex
@InProceedings{TemelCAV2020, author="Temel, Mertcan and Slobodova, Anna and Hunt, Warren A.", editor="Lahiri, Shuvendu K. and Wang, Chao", title="Automated and Scalable Verification of Integer Multipliers", booktitle="Computer Aided Verification", year="2020", publisher="Springer International Publishing", address="Cham", pages="485--507", isbn="978-3-030-53288-8", doi="10.1007/978-3-030-53288-8_23" }
- Abstract
- Mertcan Temel "RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2".
ACL2 Workshop 2020 (ACL2-2020), 13 pages, EPTCS 2020.
- Abstract
RP-Rewriter (Retain-Property) is a verified clause processor that can use some of the existing ACL2 rewrite rules to prove conjectures through term rewriting. Optimized for conjectures that can expand into large terms, the rewriter tries to mimic some of the ACL2 rewriting heuristics but also adds some extra features. It can attach side-conditions to terms that help the rewriter retain properties about them and prevent possibly some very expensive backchaining. The rewriter supports user-defined complex meta rules that can return a special structure to prevent redundant rewriting. Additionally, it can store fast alists even when values are not quoted. RP-Rewriter is utilized for two applications, multiplier design proofs and SVEX simplification, which involve very large terms.
- Paper
- Slides
- Bibtex
@inproceedings{TemelACL2-2020, author = {Mertcan Temel}, editor = {Grant O. Passmore and Ruben Gamboa}, title = {RP-Rewriter: An Optimized Rewriter for Large Terms in {ACL2}}, booktitle = {Proceedings of the Sixteenth International Workshop on the {ACL2} Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020}, series = {{EPTCS}}, volume = {327}, pages = {61--74}, year = {2020}, url = {https://doi.org/10.4204/EPTCS.327.5}, doi = {10.4204/EPTCS.327.5}, timestamp = {Tue, 29 Dec 2020 18:21:25 +0100} }
- Abstract