[libre-riscv-dev] daily kan-ban update 14may2020

[Michael Nolan]

On 5/14/20 5:48 PM, Cole Poirier wrote:
> Yesterday I worked on the script that automates the build and
> installation of yosys and the various SYMByosys tools until when trying
> to compile super_prove bitbucket had an internal error failed to load
> for over half an hour. At that point I decided to try again the next
> day. Today the bitbucket is working. I had to create two patches for the
> abc-zz sub-dependency of super_prove, now super_prove compiles
> successfully. Given that this prevents the successful compilation of an
> entire yosys tool, should I make a PR with these small but significant
> patches or should I just be satisfied that it now works for us and move
> on? The abc-zz dependecy lives in a bitbucket repo
> (https://bitbucket.org/niklaseen/abc-zz/src/default/) that is over five
> years old and the super_prove bitbucket repo's
> (https://bitbucket.org/sterin/super_prove_build/src/default/) most
> recent commit is in 2017. Given this, what would you advise I do with
> regard to a PR/moving on?
>
I've never been able to/never bothered to install super_prove or aiger 
for use with SymbiYosys. For running the formal proofs Libre-Soc has 
done, I think you only need one of the SMTBMC solvers (my recommendation 
is yices2).

--Michael