diff --git a/SymbiYosys/Dockerfile b/SymbiYosys/Dockerfile deleted file mode 100644 index e32609e..0000000 --- a/SymbiYosys/Dockerfile +++ /dev/null @@ -1,112 +0,0 @@ -FROM ubuntu:18.04 - -RUN apt-get update && \ - apt-get upgrade -y && \ - apt-get install -y \ - build-essential \ - clang \ - bison \ - flex \ - libreadline-dev \ - gawk \ - tcl-dev \ - libffi-dev \ - git \ - mercurial \ - graphviz \ - xdot \ - pkg-config \ - python \ - python3 \ - libftdi-dev \ - gperf \ - libboost-program-options-dev \ - autoconf \ - libgmp-dev \ - cmake \ - make \ - wget \ - libpython2.7 && \ - adduser symbiyosys --gecos "" --disabled-login - -RUN cd /home/symbiyosys && \ - git clone https://github.com/cliffordwolf/yosys.git yosys && \ - cd yosys && \ - make -j$(nproc) && \ - make install && \ - cd /home/symbiyosys && \ - git clone https://github.com/cliffordwolf/SymbiYosys.git SymbiYosys && \ - cd SymbiYosys && \ - make install && \ - cd /home/symbiyosys && \ - git clone https://github.com/Z3Prover/z3.git z3 && \ - cd z3 && \ - python scripts/mk_make.py && \ - cd build && \ - make -j$(nproc) && \ - make install && \ - cd /home/symbiyosys && \ - git clone https://github.com/SRI-CSL/yices2.git yices2 && \ - cd yices2 && \ - autoconf && \ - ./configure && \ - make -j$(nproc) && \ - make install && \ - cd /home/symbiyosys && \ - git clone https://bitbucket.org/arieg/extavy.git && \ - cd extavy && \ - git submodule update --init && \ - mkdir build; cd build && \ - cmake -DCMAKE_BUILD_TYPE=Release .. && \ - make -j$(nproc) && \ - cp avy/src/avy /usr/local/bin/ && \ - cp avy/src/avybmc /usr/local/bin/ && \ - cd /home/symbiyosys && \ - git clone https://github.com/boolector/boolector && \ - git clone https://github.com/arminbiere/lingeling boolector/deps/lingeling && \ - git clone https://github.com/boolector/btor2tools boolector/deps/btor2tools && \ - ( cd boolector/deps/lingeling && ./configure.sh -fPIC && make -j$(nproc); ) && \ - ( cd boolector/deps/btor2tools && ./configure.sh -fPIC && make -j$(nproc); ) && \ - ( cd boolector && ./configure.sh && cd build && make -j$(nproc); ) && \ - cp boolector/build/bin/boolector /usr/local/bin/ && \ - cp boolector/build/bin/btor* /usr/local/bin/ && \ - cp boolector/deps/btor2tools/bin/btorsim /usr/local/bin/ && \ - cd /home/symbiyosys && \ - wget https://downloads.bvsrc.org/super_prove/super_prove-hwmcc17_final-2-d7b71160dddb-Ubuntu_14.04-Release.tar.gz && \ - tar xzf super_prove-hwmcc17_final-2-d7b71160dddb-Ubuntu_14.04-Release.tar.gz -C /usr/local/ && \ - echo '#!/bin/bash' >> /usr/local/bin/suprove && \ - echo 'tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi' >> /usr/local/bin/suprove && \ - echo 'exec /usr/local/super_prove/bin/${tool}.sh "$@"' >> /usr/local/bin/suprove && \ - chmod +x /usr/local/bin/suprove && \ - rm -rf yosys SymbiYosys z3 yices2 extavy boolector super_prove* - -RUN apt-get purge -y \ - build-essential \ - clang \ - bison \ - flex \ - libreadline-dev \ - gawk \ - libffi-dev \ - git \ - mercurial \ - graphviz \ - xdot \ - pkg-config \ - libftdi-dev \ - gperf \ - libboost-program-options-dev \ - autoconf \ - libgmp-dev \ - cmake \ - wget && \ - apt-get clean -y && \ - apt-get autoclean -y && \ - apt-get autoremove -y - - -USER symbiyosys -WORKDIR /home/symbiyosys - -RUN mkdir work -VOLUME /home/symbiyosys/work diff --git a/ghdl-formal.Dockerfile b/ghdl-formal.Dockerfile new file mode 100644 index 0000000..508b9de --- /dev/null +++ b/ghdl-formal.Dockerfile @@ -0,0 +1,66 @@ +## GHDL ## + +FROM symbiyosys as symbiyosys-ghdl + +ARG LLVM_VER="7" +ARG GNAT_VER="8" + +RUN apt-get update -qq && \ + DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ + gnat \ + zlib1g-dev \ + llvm-dev && \ + apt-get autoclean && apt-get clean && apt-get -y autoremove && \ + rm -rf /var/lib/apt/lists/* + +# Build GHDL +RUN cd /root && \ + mkdir ghdl && \ + cd ghdl && \ + curl https://codeload.github.com/ghdl/ghdl/tar.gz/master | tar xzf - --strip-components=1 && \ + ./configure --enable-synth --prefix=/opt/ghdl --with-llvm-config=llvm-config-$LLVM_VER && \ + make && \ + make install + + +## GHDLSYNTH-BETA ## + +FROM symbiyosys-ghdl AS symbiyosys-ghdlsynth + +# Build ghdlsynth-beta +RUN cd /root && \ + mkdir ghdlsynth-beta && \ + cd ghdlsynth-beta && \ + curl https://codeload.github.com/tmeissner/ghdlsynth-beta/tar.gz/tests | tar xzf - --strip-components=1 && \ + make GHDL=/opt/ghdl/bin/ghdl YOSYS_CONFIG=/opt/yosys/bin/yosys-config && \ + make install GHDL=/opt/ghdl/bin/ghdl YOSYS_CONFIG=/opt/yosys/bin/yosys-config + + +# GHDL-formal + +FROM debian:buster-slim AS ghdl-formal + +# Get runtime dependencies +RUN apt-get update -qq && \ + DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ + ca-certificates \ + libreadline7 \ + libtcl8.6 \ + libgnat-8 \ + make \ + python3 && \ + apt-get autoclean && apt-get clean && apt-get -y autoremove && \ + update-ca-certificates && \ + rm -rf /var/lib/apt/lists/* + +# copy build artifacts +COPY --from=symbiyosys-ghdlsynth /opt/ghdl /opt/ghdl +COPY --from=symbiyosys-ghdlsynth /opt/symbiyosys /opt/symbiyosys +COPY --from=symbiyosys-ghdlsynth /opt/yosys /opt/yosys +COPY --from=symbiyosys-ghdlsynth /opt/z3 /opt/z3 +COPY --from=symbiyosys-ghdlsynth /opt/yices2 /opt/yices2 +COPY --from=symbiyosys-ghdlsynth /opt/cvc4 /opt/cvc4 +COPY --from=symbiyosys-ghdlsynth /opt/boolector /opt/boolector + +# 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:$PATH" diff --git a/symbiyosys.Dockerfile b/symbiyosys.Dockerfile new file mode 100644 index 0000000..ac6ae29 --- /dev/null +++ b/symbiyosys.Dockerfile @@ -0,0 +1,84 @@ +FROM debian:buster-slim as yosys + +## YOSYS ## + +# Get yosys dependencies +RUN apt-get update -qq && \ + DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ + ca-certificates \ + gcc \ + make \ + bison \ + flex \ + libreadline-dev \ + gawk \ + tcl-dev \ + libffi-dev \ + graphviz \ + xdot \ + pkg-config \ + python3 \ + libboost-system-dev \ + libboost-python-dev \ + libboost-filesystem-dev \ + clang \ + git && \ + apt-get autoclean && apt-get clean && apt-get -y autoremove && \ + update-ca-certificates && \ + rm -rf /var/lib/apt/lists/* && \ + cd /root && \ + git clone https://github.com/YosysHQ/yosys.git yosys && \ + cd yosys && \ + git clone https://github.com/berkeley-abc/abc.git abc && \ + make -j$(nproc) PREFIX=/opt/yosys && \ + make install PREFIX=/opt/yosys + + +# SymbiYosys, Solvers + +FROM yosys AS symbiyosys + +RUN apt-get update -qq && \ + DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ + autoconf \ + gperf \ + cmake \ + curl \ + libgmp-dev && \ + apt-get autoclean && apt-get clean && apt-get -y autoremove && \ + rm -rf /var/lib/apt/lists/* && \ + cd /root && \ + git clone https://github.com/YosysHQ/SymbiYosys.git symbiyosys && \ + cd symbiyosys && \ + make install PREFIX=/opt/symbiyosys && \ + cd .. && \ + git clone https://github.com/Z3Prover/z3.git z3 && \ + cd z3 && \ + python scripts/mk_make.py && \ + cd build && \ + make -j$(nproc) PREFIX=/opt/z3 && \ + make install PREFIX=/opt/z3 && \ + cd /root && \ + git clone https://github.com/SRI-CSL/yices2.git yices2 && \ + cd yices2 && \ + autoconf && \ + ./configure --prefix=/opt/yices2 && \ + make -j$(nproc) && \ + make install && \ + cd /opt && \ + mkdir cvc4 && mkdir cvc4/bin && \ + curl -L -o cvc4/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt && \ + chmod +x cvc4/bin/cvc4 && \ + cd /root && \ + git clone https://github.com/boolector/boolector && \ + cd boolector && \ + ./contrib/setup-btor2tools.sh && \ + ./contrib/setup-lingeling.sh && \ + ./configure.sh && \ + make -C build -j$(nproc) PREFIX=/opt/boolector && \ + cd /root/boolector && \ + mkdir /opt/boolector && \ + mkdir /opt/boolector/bin && \ + cp build/bin/boolector /opt/boolector/bin/ && \ + cp build/bin/btor* /opt/boolector/bin/ && \ + cp deps/btor2tools/bin/btorsim /opt/boolector/bin/