Skip to content

Commit

Permalink
updated bitwuzla commit hash / version (#461)
Browse files Browse the repository at this point in the history
Tested locally, this doesn't segfault when including `bsg_dff.sv` and
other files.

I'm going to keep doing further testing to make sure this change doesn't
break anything.

### What this PR does:
Updates the version of Bitwuzla (SMT solver used by Rosette) to the most
recent version.

### How this PR does it:
In `dependencies.sh`, line 27 defines the Bitwuzla commit hash that's
used by Lakeroad when building everything with Docker.

> `export BITWUZLA_COMMIT_HASH="..."`

I updated the Bitwuzla commit hash to the most recent version, as of
Aug. 21 2024.

### Updates
_Aug 28 2024:_ [An issue in Bitwuzla has been opened that's possibly
related to this](bitwuzla/bitwuzla#121)

---------

Co-authored-by: Gus Smith <[email protected]>
  • Loading branch information
cknizek and gussmith23 authored Sep 5, 2024
1 parent 437a49d commit 55ccee5
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 5 deletions.
2 changes: 1 addition & 1 deletion dependencies.sh
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
export STP_USER_AND_REPO="stp/stp"
export STP_COMMIT_HASH="918e55c011df5226d293d5f7a784507e03774e28"
export YICES2_COMMIT_HASH="5326f0d645df6e38ae6e7d944381d01ba7d805ab"
export BITWUZLA_COMMIT_HASH="b655bc0cde570258367bf8f09a113bc7b95e46e9"
export BITWUZLA_COMMIT_HASH="9e5d7d82b0a0bfd3dc838eb3c3936acad500dc97"
export RACKET_FMT_COMMIT_HASH="7d0a3dfff3a6cacfb59972a56d476556f89a0b1b"
export YOSYS_COMMIT_HASH="70d35314dbd7521870047ed607897f22dc48cbc3"
export CVC5_COMMIT_HASH="1d05a49387c041dba17f85f3c4e738b4b388ace2"
Expand Down
6 changes: 2 additions & 4 deletions integration_tests/lakeroad/combinational_multiplier_xilinx.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// RUN: (racket $LAKEROAD_DIR/bin/main.rkt \
// RUN: --solver bitwuzla \
// RUN: racket $LAKEROAD_DIR/bin/main.rkt \
// RUN: --solver yices \
// RUN: --verilog-module-filepath %s \
// RUN: --architecture xilinx-ultrascale-plus \
// RUN: --template dsp \
Expand All @@ -11,8 +11,6 @@
// RUN: --input-signal a:16 \
// RUN: --input-signal b:16 \
// RUN: --timeout 90 \
// RUN: || true) \
// RUN: 2>&1 \
// RUN: | FileCheck %s

module combinational_multiplier(input [15:0] a, b, output [15:0] p);
Expand Down

0 comments on commit 55ccee5

Please sign in to comment.