Dockerfile restructure + Lakeroad Yosys plugin

.gitmodules

@@ -1,9 +1,6 @@
 [submodule "lakeroad-private"]
 	path = lakeroad-private
 	url = [email protected]:uwsampl/lakeroad-private
-[submodule "bitwuzla"]
-	path = bitwuzla
-	url = [email protected]:bitwuzla/bitwuzla.git
 [submodule "lakeroad-egglog/yosys"]
 	path = lakeroad-egglog/yosys
 	url = [email protected]:uwsampl/yosys

Dockerfile

@@ -1,15 +1,20 @@
 # syntax=docker/dockerfile-upstream:master-labs
 # The above enables use of ADD of git repo.
+
 FROM ubuntu:22.04
+ARG MAKE_JOBS=2
+SHELL ["/bin/bash", "-c"] 
 
 # Update, get add-apt-repository, add PPA for Racket, update again.
 RUN apt update \
   &&  apt install -y software-properties-common \
   &&  add-apt-repository ppa:plt/racket \
   && apt update
 
-## Install dependencies
-# apt dependencies
+# Install apt dependencies
+# `noninteractive` prevents the tzdata package from asking for a timezone on the
+# command line.
+ENV DEBIAN_FRONTEND=noninteractive
 RUN apt install -y \
   autoconf \
   bison \
@@ -19,11 +24,12 @@ RUN apt install -y \
   flex \
   g++ \
   git \
-  git \
+  libboost-filesystem-dev \
   libfl-dev \
   libfl2 \
   libgmp-dev \
   libgoogle-perftools-dev \
+  libreadline-dev \
   libssl-dev \
   libzmq3-dev \
   llvm-14 \
@@ -37,6 +43,8 @@ RUN apt install -y \
   python3 \
   python3-pip \
   racket \
+  tcl \
+  tcl8.6-dev \
   wget \
   zlib1g \
   zlib1g-dev
@@ -59,42 +67,51 @@ ENV PATH="/root/.local/bin:${PATH}"
 # Install a bunch of useful tools from prebuilt binaries. Thanks to YosysHQ for
 # making this available!
 #
-# We currently use the following binaries from oss-cad-suite:
-# yosys, verilator, cvc5, boolector.
-#
 # If we get an error here, we likely just need to add other branches for other
 # architectures.
 #
-# TODO(@gussmith23): Could shrink Docker image by deleting unneeded binaries.
+# TODO(@gussmith23): Could shrink Docker image by deleting a bunch of uneeded
+# binaries, or only taking the binaries we need. However, I found that moving
+# stuff out of oss-cad-suite causes things to break.
 WORKDIR /root
-RUN if [ "$(uname -m)" = "x86_64" ] ; then \
-  wget https://github.com/YosysHQ/oss-cad-suite-build/releases/download/2023-08-06/oss-cad-suite-linux-x64-20230806.tgz -q -O oss-cad-suite.tgz; \
+ADD dependencies.sh /root/dependencies.sh
+RUN source /root/dependencies.sh \
+  && if [ "$(uname -m)" = "x86_64" ] ; then \
+  wget https://github.com/YosysHQ/oss-cad-suite-build/releases/download/$OSS_CAD_SUITE_DATE/oss-cad-suite-linux-x64-$(echo $OSS_CAD_SUITE_DATE | tr -d "-").tgz -q -O oss-cad-suite.tgz; \
   else \
   exit 1; \
   fi \
-  && tar xf oss-cad-suite.tgz
-ENV PATH="/root/oss-cad-suite/bin:${PATH}"
+  && tar xf oss-cad-suite.tgz \
+  && rm oss-cad-suite.tgz \
+  # Delete binaries we don't need (and that we explicitly build other versions
+  # of).
+  && rm oss-cad-suite/bin/yosys \
+  && rm oss-cad-suite/bin/bitwuzla
+# Make sure that .local/bin has precedence over oss-cad-suite/bin. I realize
+# we add ./local/bin to the PATH twice, but I just want to document that we want
+# things in .local/bin to take precedence, and duplicate PATH entries won't
+# break anything.
+ENV PATH="/root/.local/bin:/root/oss-cad-suite/bin:${PATH}"
 
 # pip dependencies
 WORKDIR /root/lakeroad
 ADD requirements.txt requirements.txt
 RUN pip install -r requirements.txt
 
-# Build Bitwuzla from version tracked in submodule.
+# Build Bitwuzla.
 WORKDIR /root
-ARG MAKE_JOBS=2
-ADD bitwuzla bitwuzla
-RUN cd bitwuzla \
-  && ./configure.py \
+RUN source /root/dependencies.sh \
+  && mkdir bitwuzla \
+  && wget -qO- https://github.com/bitwuzla/bitwuzla/archive/$BITWUZLA_COMMIT_HASH.tar.gz | tar xz -C bitwuzla --strip-components=1 \
+  && cd bitwuzla \
+  && ./configure.py --prefix=/root/.local \
   && cd build \
-  && ninja -j${MAKE_JOBS}
-# Put it on the path. Note that there's a bitwuzla in oss-cad-suite, so we need
-# to make sure this one takes precedence.
-ENV PATH="/root/bitwuzla/build/src/main/:${PATH}"
+  && ninja -j${MAKE_JOBS} \
+  && ninja install \
+  && rm -rf /root/bitwuzla
 
 # Install raco (Racket) dependencies. 
 WORKDIR /root
-ARG FMT_COMMIT_HASH=bd44477
 RUN \
   # First, fix https://github.com/racket/racket/issues/2691 by building the
   # docs.
@@ -108,7 +125,8 @@ RUN \
   && cd /root \
   && git clone https://github.com/sorawee/fmt \
   && cd fmt \
-  && git checkout ${FMT_COMMIT_HASH} \
+  && source /root/dependencies.sh \
+  && git checkout $RACKET_FMT_COMMIT_HASH \
   && raco pkg install --deps search-auto --batch
 
 # Install Rust
@@ -144,37 +162,37 @@ ENV LAKEROAD_PRIVATE_DIR=/root/lakeroad/lakeroad-private
 
 # Build STP.
 WORKDIR /root
-ENV STP_URL="https://github.com/stp/stp/archive/0510509a85b6823278211891cbb274022340fa5c.tar.gz"
 RUN apt-get install -y git cmake bison flex libboost-all-dev python2 perl && \
-  wget ${STP_URL} -nv -O stp.tar.gz && \
-  mkdir stp && \
-  tar xzf stp.tar.gz -C stp --strip-components=1 && \
-  cd stp && \
+  source /root/dependencies.sh && \
+  mkdir stp && cd stp && \
+  wget -qO- https://github.com/stp/stp/archive/$STP_COMMIT_HASH.tar.gz | tar xz --strip-components=1 && \
   ./scripts/deps/setup-gtest.sh && \
   ./scripts/deps/setup-outputcheck.sh && \
   ./scripts/deps/setup-cms.sh && \
   ./scripts/deps/setup-minisat.sh && \
   mkdir build && \
   cd build && \
-  cmake .. && \
-  cmake --build .
+  cmake .. -DCMAKE_INSTALL_PREFIX=/root/.local && \
+  make -j ${MAKE_JOBS}
+# TODO(@gussmith23): Install and delete folder once
+# https://github.com/stp/stp/issues/479 is fixed.
+# make install && \
+# rm -rf /root/stp
+# And after that we also don't need to add STP to the path.
 ENV PATH="/root/stp/build:${PATH}"
 
-# Build Yices2.
+# Build Yosys.
 WORKDIR /root
-ENV YICES2_URL="https://github.com/SRI-CSL/yices2/archive/e27cf308cffb0ecc6cc7165c10e81ca65bc303b3.tar.gz"
-RUN apt-get install -y gperf && \
-  wget ${YICES2_URL} -nv -O yices2.tar.gz && \
-  mkdir yices2 && \
-  tar xvf yices2.tar.gz -C yices2 --strip-components=1 && \
-  cd yices2 && \
-  autoconf && \
-  ./configure && \
-  make && \
-  # If this line fails, it's presumably because we're on a different architecture.
-  [ -d build/x86_64-pc-linux-gnu-release/bin ]
-ENV PATH="/root/yices2/build/x86_64-pc-linux-gnu-release/bin/:${PATH}"
-
+RUN source /root/dependencies.sh \
+  && mkdir yosys && cd yosys \
+  && wget -qO- https://github.com/YosysHQ/yosys/archive/$YOSYS_COMMIT_HASH.tar.gz | tar xz --strip-components=1 \
+  && PREFIX="/root/.local" CPLUS_INCLUDE_PATH="/usr/include/tcl8.6/:$CPLUS_INCLUDE_PATH" make config-gcc \
+  && PREFIX="/root/.local" CPLUS_INCLUDE_PATH="/usr/include/tcl8.6/:$CPLUS_INCLUDE_PATH" make -j ${MAKE_JOBS} install \
+  && rm -rf /root/yosys
+
+# Build Yosys plugin.
+WORKDIR /root/lakeroad/yosys-plugin
+RUN make -j ${MAKE_JOBS}
 
 WORKDIR /root/lakeroad
 CMD [ "/bin/bash", "run-tests.sh" ]

README.md

@@ -137,3 +137,9 @@ TODO(@gussmith23): this is unintuitive and not user-friendly.
 The [./import_all_primitives.sh](./import_all_primitives.sh) script uses sed, which it expects to be GNU sed. On Mac, you can install GNU sed via Homebrew and add it to your PATH temporarily or permanently.
 
 TODO(@gussmith23): Find better cross-platform regex. I thought Perl might be the answer.
+
+## Yosys Plugin
+
+Lakeroad is usable via a Yosys plugin, which can be built separately and loaded directly into your existing Yosys installation. The plugin is located in [./yosys-plugin/](./yosys-plugin/) and can be built using the Makefile in that directory. The plugin can be loaded into Yosys using Yosys's `-m` option, e.g. `yosys -m lakeroad.so ...`. An example of this can be seen in [this integration test.](./integration_tests/lakeroad/xilinx_muladd_0_stage_signed_8_bit_yosys_plugin.sv)
+
+Note: the Lakeroad plugin needs to be built in the same environment (i.e. same glibc version) as the Yosys executable it's being loaded into. This can be an issue e.g. when using the Yosys executable in `oss-cad-suite`. The easiest way to prevent this is to build Yosys yourself using their directions.

dependencies.sh

@@ -0,0 +1,29 @@
+#!/bin/sh
+# This script exports a number of variables that help to pin the versions of
+# various Lakeroad dependencies.
+#
+# To use, source this script before running relevant commands e.g. in a
+# Dockerfile.
+#
+# This is just one possible way to implement dependency tracking. Some of the
+# other options are:
+# - No tracking at all. E.g. in the Dockerfile, we could clone STP at a specific
+#   commit, using a "magic constant" commit hash. This isn't ideal, because if
+#   we use STP elsewhere (e.g. in the evaluation) we have to make sure we keep
+#   the commit hashes in sync.
+# - Git submodules. This is very similar to what we've chosen to do, but it's
+#   more directly supported by Git. For example, we used to have Bitwuzla be a
+#   submodule of Lakeroad. This avoids the need to sync commit hashes as in the
+#   first option. However, it's a bit overkill to add a full repository as a
+#   submodule when we only need the resulting binary.
+#
+# This option is essentially a lighter-weight version of submodules. We track
+# the commit hashes of the dependencies we need, but nothing additional is
+# cloned on a `git clone --recursive`.
+
+export STP_COMMIT_HASH="0510509a85b6823278211891cbb274022340fa5c"
+export YICES2_COMMIT_HASH="e27cf308cffb0ecc6cc7165c10e81ca65bc303b3"
+export BITWUZLA_COMMIT_HASH="b655bc0cde570258367bf8f09a113bc7b95e46e9"
+export OSS_CAD_SUITE_DATE="2023-08-06"
+export RACKET_FMT_COMMIT_HASH=bd44477
+export YOSYS_COMMIT_HASH="70d35314dbd7521870047ed607897f22dc48cbc3"

integration_tests/lakeroad/xilinx_muladd_0_stage_signed_8_bit_yosys_plugin.sv

@@ -0,0 +1,53 @@
+// RUN: outfile=$(mktemp)
+// RUN: yosys -m "$LAKEROAD_DIR/yosys-plugin/lakeroad.so" -p " \
+// RUN:  read_verilog %s; \
+// RUN:  hierarchy -top in_module; \
+// RUN:  lakeroad in_module; \
+// RUN:  rename in_module out_module; \
+// RUN:  write_verilog $outfile"
+// RUN: FileCheck %s < $outfile
+// RUN: if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
+// RUN:   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
+// RUN:   exit 0; \
+// RUN: else \
+// RUN:   python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
+// RUN:    --test_module_name out_module \
+// RUN:    --ground_truth_module_name in_module \
+// RUN:    --max_num_tests=10000 \
+// RUN:    --verilog_filepath $outfile \
+// RUN:    --verilog_filepath %s \
+// RUN:    --initiation_interval 0 \
+// RUN:    --output_signal out:8 \
+// RUN:    --input_signal a:8 \
+// RUN:    --input_signal b:8 \
+// RUN:    --input_signal c:8 \
+// RUN:    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
+// RUN:    --verilator_extra_arg='-DXIL_XECLIB' \
+// RUN:    --verilator_extra_arg='-Wno-UNOPTFLAT' \
+// RUN:    --verilator_extra_arg='-Wno-LATCH' \
+// RUN:    --verilator_extra_arg='-Wno-WIDTH' \
+// RUN:    --verilator_extra_arg='-Wno-STMTDLY' \
+// RUN:    --verilator_extra_arg='-Wno-CASEX' \
+// RUN:    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
+// RUN:    --verilator_extra_arg='-Wno-PINMISSING'; \
+// RUN: fi
+
+(* template = "dsp" *) 
+(* architecture = "xilinx-ultrascale-plus" *) 
+(* pipeline_depth = 0 *)
+module in_module(
+	(* data *)
+	input signed [7:0] a,
+	(* data *)
+	input signed [7:0] b,
+	(* data *)
+	input signed [7:0] c,
+	(* out *)
+	output [7:0] out);
+
+	assign out = (a * b) + c;
+endmodule
+
+// CHECK: module out_module(a, b, c, out);
+// CHECK:   DSP48E2 #(
+// CHECK: endmodule

yosys-plugin/.gitignore

@@ -0,0 +1,4 @@
+
+lakeroad.d
+lakeroad.so
+lakeroad.so.dSYM/

yosys-plugin/Makefile

@@ -0,0 +1,7 @@
+lakeroad.so: lakeroad.cc
+	$(CXX) $(shell yosys-config --cxxflags --ldflags) -shared -o $@ lakeroad.cc -lboost_filesystem
+
+clean:
+	rm -rfv *.d *.o lakeroad.so*
+
+-include *.d