search

hdl / conda-eda

Conda recipes for FPGA EDA tools for simulation, synthesis, place and route and bitstream generation.
https://anaconda.org/LiteX-Hub
Apache License 2.0
94 stars 27 forks source link

Add package for z3 and boolector for formal? #5

Open RobertBaruch opened 4 years ago

RobertBaruch commented 4 years ago

The Z3 solver for formal verification is quite fast (on some platforms) compared to the default for symbiyosys. On other platforms, boolector is better.

Compilation instructions at https://symbiyosys.readthedocs.io/en/latest/quickstart.html

I'd try to contribute if someone could point me to a clear step-by-step guide. I can also just try to keep attempting pull requests and seeing what the errors from Travis are :)

mithro commented 4 years ago

You can test locally, ./conda-env.sh build <path to your meta file> then once that works you do the Travis thing until green.

RobertBaruch commented 4 years ago

Hmm, now that I finally have docker locally working and compiling things, it seems that in building formal/symbiyosys, z3 and boolector are also built anyway. So obsoleting this issue.

mithro commented 4 years ago

@RobertBaruch I'm actually going to reopen this as z3 and boolector probably should be their own packages.

RobertBaruch commented 4 years ago

I'll take a shot at this.

RobertBaruch commented 4 years ago

I haven't been able to figure out how to compile z3 on windows. It's possible, but relies on a Python script from z3: python mk_make.py, which creates the appropriate makefiles for your OS. The problem is that the script relies on os.name to detect the OS, and it always comes up as nt, which is Windows, which generates a makefile for nmake, which I can't figure out how to install using conda.

Apparently the script could theoretically detect Mingw, but I don't know how to get python to run under conda while also reporting os.name as posix.

RobertBaruch commented 4 years ago

The alternative is just to download the built z3 windows version -- after all, why build z3 if it's already built -- but I have no idea how to conda, so I also have no idea how to just repackage a release for conda.

RobertBaruch commented 4 years ago

Welp, I have some conda files that Travis seems to feel compiles z3 for OSX, Linux, and Windows. Unfortunately I ended up having to pin the release at 4.8.7 because there doesn't seem to be an easy way to compile for Windows. So instead it compiles for OSX and Linux, and just downloads the built version from github for Windows.

Will work on boolector now.

RobertBaruch commented 4 years ago

Was able to get z3 compiling under Windows, so we can compile z3 from head. Still working on boolector for Windows.