Skip to content

Commit

Permalink
Dockerfile restructure + Lakeroad Yosys plugin (#408)
Browse files Browse the repository at this point in the history
This PR does two things that are only slightly related (sorry about
that):
- Introduces Lakeroad Yosys plugin, plus tests and documentation
- Restructures/simplifies/solidifies the Dockerfile

The Lakeroad Yosys plugin is a plugin for the Yosys synthesis tool which
calls Lakeroad to compile Verilog modules. During the process of adding
the plugin into CI, I realized we needed to build Yosys from source,
which led me to restructuring the Dockerfile.

The restructure of the Dockerfile does a few things:
- Moves dependencies into an explicit file (rather than adhoc or git
submodules)
- Pulls specific binaries out of oss-cad-suite and deletes the unneeded
ones
  • Loading branch information
gussmith23 authored Dec 19, 2023
1 parent f35e24e commit 3c79e7a
Show file tree
Hide file tree
Showing 9 changed files with 335 additions and 47 deletions.
3 changes: 0 additions & 3 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -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
104 changes: 61 additions & 43 deletions Dockerfile
Original file line number Diff line number Diff line change
@@ -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 \
Expand All @@ -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 \
Expand All @@ -37,6 +43,8 @@ RUN apt install -y \
python3 \
python3-pip \
racket \
tcl \
tcl8.6-dev \
wget \
zlib1g \
zlib1g-dev
Expand All @@ -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.
Expand All @@ -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
Expand Down Expand Up @@ -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" ]
6 changes: 6 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
1 change: 0 additions & 1 deletion bitwuzla
Submodule bitwuzla deleted from b655bc
29 changes: 29 additions & 0 deletions dependencies.sh
Original file line number Diff line number Diff line change
@@ -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"
Original file line number Diff line number Diff line change
@@ -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
4 changes: 4 additions & 0 deletions yosys-plugin/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@

lakeroad.d
lakeroad.so
lakeroad.so.dSYM/
7 changes: 7 additions & 0 deletions yosys-plugin/Makefile
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit 3c79e7a

Please sign in to comment.