Bit-Level Optimized Constant Multiplication Using Boolean Satisfiability

doi:10.1109/TCSI.2023.3327814

2024-01-01

PRE

Nicolai Fiege *

Martin Kumm

Peter Zipf

DOI：10.1109/TCSI.2023.3327814

原文链接

原文求助

摘要

En 中文

Multiplierless constant multiplication using bit-shifts, additions and subtractions has been an active research topic in the last decades. The multiplication with multiple constants, known as the multiple constant multiplication (MCM) problem, is of special interest because of its practical relevance, notably for digital filter implementation. In this work we propose to use the speed of modern Boolean satisfiability (SAT) solvers to find fast and optimal solutions. The solutions are optimal either with respect to the adder count or the bit level cost. In contrast to previous approaches, we also consider negative fundamentals that are sometimes cheaper to realize than their positive counterparts leading to more compact hardware implementations. Our experiments show that our approach is able to find optimal single constant multiplication (SCM) and MCM circuits for practically relevant test instances in reasonable time. We also prove the necessity for the post-add right shift operation for SCM. Using our SAT formulation to enumerate all possible implementations for some of our test instances we show the importance of considering bit-level costs and negative fundamentals when solving MCM problems.

Keyword:

Circuit optimization

fixed-point arithmetic

Boolean satisfiability