Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Higher radix multiplier encoding #7991

Draft
wants to merge 4 commits into
base: develop
Choose a base branch
from

Conversation

tautschnig
Copy link
Collaborator

The Radix-4 multiplier pre-computes products for x * 0 (zero), x * 1 (x), x * 2 (left-shift x), x * 3 (x * 2 + x) to reduce the number of sums by a factor of 2. Radix-8 extends this up to x * 7 (reducing sums by a factor of 3), and Radix-16 up to x * 15 (reducing sums by a factor of 4). This modified approach to computing partial products can be freely combined with different (tree) reduction schemes.

Benchmarking results can be found at
https://tinyurl.com/multiplier-comparison (shortened URL for https://docs.google.com/spreadsheets/d/197uDKVXYRVAQdxB64wZCoWnoQ_TEpyEIw7K5ctJ7taM/). The data suggests that combining Radix-8 partial product pre-computation with Dadda's reduction can yield substantial performance gains while not substantially regressing in other benchmark/solver pairs.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig marked this pull request as draft November 1, 2023 11:05
@tautschnig tautschnig self-assigned this Nov 1, 2023
@tautschnig tautschnig force-pushed the feature/multiplier-encoding branch 2 times, most recently from c5111f1 to 354bb4e Compare November 1, 2023 20:21
@tautschnig tautschnig marked this pull request as ready for review November 1, 2023 21:03
@tautschnig tautschnig removed their assignment Nov 1, 2023
Copy link

codecov bot commented Nov 1, 2023

Codecov Report

Attention: 10 lines in your changes are missing coverage. Please review.

Comparison is base (74075ec) 79.09% compared to head (354bb4e) 78.63%.

❗ Current head 354bb4e differs from pull request most recent head ffe136e. Consider uploading reports for the commit ffe136e to get more accurate results

Files Patch % Lines
src/solvers/flattening/bv_utils.cpp 93.97% 10 Missing ⚠️
Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #7991      +/-   ##
===========================================
- Coverage    79.09%   78.63%   -0.46%     
===========================================
  Files         1699     1701       +2     
  Lines       196512   196571      +59     
===========================================
- Hits        155428   154575     -853     
- Misses       41084    41996     +912     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@tautschnig tautschnig self-assigned this Nov 16, 2023
@tautschnig tautschnig marked this pull request as draft October 28, 2024 09:35
The Radix-4 multiplier pre-computes products for x * 0 (zero), x * 1
(x), x * 2 (left-shift x), x * 3 (x * 2 + x) to reduce the number of
sums by a factor of 2. Radix-8 extends this up to x * 7 (reducing sums
by a factor of 3), and Radix-16 up to x * 15 (reducing sums by a factor
of 4). This modified approach to computing partial products can be
freely combined with different (tree) reduction schemes.

Benchmarking results can be found at
https://tinyurl.com/multiplier-comparison (shortened URL for
https://docs.google.com/spreadsheets/d/197uDKVXYRVAQdxB64wZCoWnoQ_TEpyEIw7K5ctJ7taM/).
The data suggests that combining Radix-8 partial product pre-computation
with Dadda's reduction can yield substantial performance gains while not
substantially regressing in other benchmark/solver pairs.
We cannot accomplish a reduction in bit widths for we do not know
upfront whether computing z_0 (the product of the lower halves) requires
less than the full bit width to represent its multiplication result.
Implements the algorithm of Section 4 of "Further Steps Down The Wrong
Path : Improving the Bit-Blasting of Multiplication" (see
https://ceur-ws.org/Vol-2908/short16.pdf).
Implements a symbolic version of the algorithm proposed by Schönhage and
Strassen in "Schnelle Multiplikation großer Zahlen", Computing, 7, 1971.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant