Replace monolitic Dockerfiles by modular ones for SymbiYosys & GHDl(-synth)

SymbiYosys/Dockerfile

@@ -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

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"

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/