Bug 891 - fix cvc5 on ppc64le
Summary: fix cvc5 on ppc64le
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Source Code (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- major
Assignee: Jacob Lifshay
URL:
Depends on:
Blocks:
 
Reported: 2022-07-13 05:30 BST by Jacob Lifshay
Modified: 2023-06-25 23:22 BST (History)
3 users (show)

See Also:
NLnet milestone: NLnet.2021.02A.052.CryptoRouter
total budget (EUR) for completion of task and all subtasks: 600
budget (EUR) for this task, excluding subtasks' budget: 600
parent task for budget allocation: 775
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:
[jacob] amount = 600 submitted = 2023-06-05 paid = 2023-06-21

Attachments
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
Comment 1 Jacob Lifshay 2022-07-13 05:46:02 BST 
tested nmigen, spec_hdl_smtlib2_real_div now passes on ppc64le with the fixed cvc5.

I pushed the fixed branch to:
https://git.libre-soc.org/?p=cvc5.git;a=summary

lkcl, you need to set that to public. once that's done, the dev-env-setup scripts can be changed to use the fix-ppc64le branch until cvc5 upstream accepts my PR.
Comment 2 Jacob Lifshay 2022-07-13 21:54:06 BST 
(In reply to Jacob Lifshay from comment #0)
> https://bugs.libre-soc.org/show_bug.cgi?id=883#c7
> 
> PR: https://github.com/cvc5/cvc5/pull/8955

The PR was merged upstream. I pushed that to our cvc5 mirror.

all that's left is updating dev-env-setup.git
Comment 3 Jacob Lifshay 2022-07-22 23:21:31 BST 
cvc5 1.0.1 was released a few days ago, it includes the ppc64le build fixes. I updated dev-env-setup.git to use that version after some testing on the talos and my desktop.

https://git.libre-soc.org/?p=dev-env-setup.git;a=blob;f=hdl-tools-yosys;h=5b54555e527669039e32d945d15236f39b04629f;hb=HEAD

unrelated: i noticed other repos (yices, z3) installed by hdl-tools-yosys use whatever is the latest commit on the upstream repos, rather than picking a particular commit/tag for reproducibility -- imho that should probably be fixed.