Bug 883 - add cvc5 and bitwuzla to hdl-yosys-tools
Summary: add cvc5 and bitwuzla to hdl-yosys-tools
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Source Code (show other bugs)
Version: unspecified
Hardware: PC Linux
: High enhancement
Assignee: Veera
URL:
Depends on: 835
Blocks:
  Show dependency treegraph
 
Reported: 2022-07-05 13:31 BST by Luke Kenneth Casson Leighton
Modified: 2022-07-22 18:26 BST (History)
2 users (show)

See Also:
NLnet milestone: NLNet.2019.10.032.Formal
total budget (EUR) for completion of task and all subtasks: 800
budget (EUR) for this task, excluding subtasks' budget: 800
parent task for budget allocation: 835
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
vklr={amount=800, submitted=2022-07-12, paid=2022-07-22}


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Comment 1 Luke Kenneth Casson Leighton 2022-07-05 13:36:29 BST
    - git clone --depth 1 -b cvc5-1.0.0 https://github.com/cvc5/cvc5.git cvc5
    - pushd cvc5
    - git rev-parse HEAD
    - ./configure.sh --poly --auto-download -DCMAKE_CXX_COMPILER=/usr/lib/ccache/g++ -DCMAKE_C_COMPILER=/usr/lib/ccache/gcc
    - cd build
    - make -j$(nproc)
    - make install
    - popd
Comment 2 Luke Kenneth Casson Leighton 2022-07-06 23:23:05 BST
 102         - git clone https://github.com/bitwuzla/bitwuzla.git bitwuzla
 103         - pushd bitwuzla
 104         - git checkout 19dd987a6e246990619751cca07996fac505fd0b
 105         - ./contrib/setup-btor2tools.sh
 106         - ./contrib/setup-symfpu.sh
 107         - ./contrib/setup-cadical.sh
 108         - ./configure.sh
 109         - cd build
 110         - make -j$(nproc)
 111         - make install
 112         - popd
Comment 3 Jacob Lifshay 2022-07-06 23:33:44 BST
(In reply to Luke Kenneth Casson Leighton from comment #2)
official build instructions:
https://github.com/bitwuzla/bitwuzla#linux-and-unix-like-os

>  110         - make -j$(nproc)
>  111         - make install

note that make install requires sudo, none of the other commands require it.

>  112         - popd
Comment 4 Veera 2022-07-12 13:43:04 BST
Added initial support for cvc5 and bitwuzla.

uri: https://git.libre-soc.org/?p=dev-env-setup.git;a=commitdiff;h=31c0963eec1866251e343b40ec0f527577c5b932

Kindly review.
Comment 5 Veera 2022-07-12 15:50:22 BST
cvc5 builds fine in PowerPC64 machine but does not runs fine.

Ran "make check" for cvc5 and got: 1% tests passed, 2936 tests failed out of 2966
Looked at running log: In most of the tests cvc5 segfaults

Currently Supported Operating Systems:
cvc5 can be built natively on Linux and macOS, cross-compilation is possible for Windows using Mingw-w64. cvc5 also supports cross-compilation for ARM64 systems. They generally recommend a 64-bit operating system.

Support for x86_64 has been checked as working.
Comment 6 Jacob Lifshay 2022-07-13 05:07:39 BST
(In reply to Veera from comment #5)
> cvc5 builds fine in PowerPC64 machine but does not runs fine.
> 
> Ran "make check" for cvc5 and got: 1% tests passed, 2936 tests failed out of
> 2966
> Looked at running log: In most of the tests cvc5 segfaults

adding -fpermissive just hid the actual problem, I figured out that antlr was being built with options making it think pointers are 32-bit because cvc5 botched their 64-bit detection logic in their cmake scripts.

I created a PR with the fix (it passed make check, but I didn't try nmigen yet)

https://github.com/cvc5/cvc5/pull/8955

fixed branch:
https://github.com/programmerjake/cvc5/tree/fix-ppc64le

lkcl, if you can create a cvc5 repo, I can push the fixed branch there too.
Comment 7 Luke Kenneth Casson Leighton 2022-07-13 05:15:39 BST
(In reply to Jacob Lifshay from comment #6)

> adding -fpermissive just hid the actual problem, I figured out that antlr
> was being built with options making it think pointers are 32-bit because
> cvc5 botched their 64-bit detection logic in their cmake scripts.

niiiice.

> lkcl, if you can create a cvc5 repo, I can push the fixed branch there too.

done. have to put this under a separate bugreport (with budget),
this one's done (and closed)