diff --git a/README.md b/README.md index 9f97abc..81343fb 100644 --- a/README.md +++ b/README.md @@ -14,6 +14,7 @@ A collection of Dockerfiles for easy use of various free & open-source tools. Ha * Boolector * Bitwuzla * Super Prove +* Avy ## ghdl-formal.Dockerfile @@ -47,6 +48,7 @@ Risc-V toolchain to develop programs for [NEORV32](https://github.com/stnolting/ * [Z3](https://github.com/Z3Prover/z3) * [Yices 2](https://yices.csl.sri.com/) * [CVC4](https://cvc4.github.io/) +* [Avy](https://bitbucket.org/arieg/extavy) * [Boolector](https://boolector.github.io/) * [Bitwuzla](https://bitwuzla.github.io/) * [Super Prove](https://github.com/berkeley-abc/super_prove) diff --git a/ghdl-formal.Dockerfile b/ghdl-formal.Dockerfile index ba6a1b0..305a224 100644 --- a/ghdl-formal.Dockerfile +++ b/ghdl-formal.Dockerfile @@ -52,6 +52,8 @@ RUN apt-get update -qq && \ make \ python3 \ libssl-dev \ + libboost-program-options1.67.0 \ + strace \ libpython2.7 && \ apt-get -y upgrade && apt-get autoclean && apt-get clean && apt-get -y autoremove && \ update-ca-certificates && \ @@ -61,4 +63,4 @@ RUN apt-get update -qq && \ COPY --from=symbiyosys-ghdlsynth /opt /opt # Enhance path variable -ENV PATH "/opt/ghdl/bin:/opt/symbiyosys/bin:/opt/yosys/bin:/opt/z3/bin:/opt/yices2/bin:/opt/cvc4/bin:/opt/boolector/bin:/opt/bitwuzla/bin:/opt/super_prove/bin:$PATH" +ENV PATH "/opt/ghdl/bin:/opt/symbiyosys/bin:/opt/yosys/bin:/opt/z3/bin:/opt/yices2/bin:/opt/avy/bin:/opt/cvc4/bin:/opt/boolector/bin:/opt/bitwuzla/bin:/opt/super_prove/bin:$PATH" diff --git a/symbiyosys.Dockerfile b/symbiyosys.Dockerfile index f3c66b8..6d63ee9 100644 --- a/symbiyosys.Dockerfile +++ b/symbiyosys.Dockerfile @@ -41,6 +41,7 @@ RUN apt-get update -qq && \ FROM yosys AS symbiyosys COPY packages/suprove /root/suprove +COPY packages/avy.patch /root/avy.patch RUN apt-get update -qq && \ DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ @@ -53,6 +54,7 @@ RUN apt-get update -qq && \ python-setuptools \ python-pip \ python-wheel \ + libboost-program-options-dev \ mercurial && \ apt-get autoclean && apt-get clean && apt-get -y autoremove && \ rm -rf /var/lib/apt/lists/* && \ @@ -113,5 +115,16 @@ RUN apt-get update -qq && \ ninja package && \ tar -C /opt -xzf super_prove*.tar.gz && \ mv /root/suprove /opt/super_prove/bin/ && \ - chmod +x /opt/super_prove/bin/suprove && \ + chmod +x /opt/super_prove/bin/suprove + +RUN cd /root && \ + git clone https://bitbucket.org/arieg/extavy.git && \ + cd extavy && \ + git checkout new_quip && \ + git submodule update --init && \ + mkdir build; cd build && \ + cmake -DCMAKE_BUILD_TYPE=Debug .. && \ + make -j$(nproc) && \ + mkdir -p /opt/avy/bin && \ + cp -r avy/src/av* /opt/avy/bin/ && \ rm -rf /root/*