Support STP and Yices2 (#400)

This PR adds support for STP and Yices2 to improve our portfolio solving. It adds - Match arm branches of solver flag parsing in`main.rkt` that allows the user to pass in STP or Yices2 as the solver. - Lines in the `lakeroad-portfolio.py` that add stp and yices2 as options for portfolio solving. Note that this PR doesn't add functionality for passing flags/solver settings to STP or Yices2; we haven't needed them yet. Closes #406 --------- Co-authored-by: Gus Smith <[email protected]>
gussmith23 · Dec 15, 2023 · e0d02d2 · e0d02d2
1 parent fbcb093
commit e0d02d2
Show file tree

Hide file tree

Showing 6 changed files with 58 additions and 89 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -150,5 +150,39 @@ RUN raco make /root/lakeroad/bin/main.rkt
 # uses LAKEROAD_PRIVATE_DIR should check if the directory exists/is nonempty first.
 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 && \
+  ./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 .
+ENV PATH="/root/stp/build:${PATH}"
+
+# Build Yices2.
+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}"
+
+
 WORKDIR /root/lakeroad
 CMD [ "/bin/bash", "run-tests.sh" ]
diff --git a/bin/lakeroad-portfolio.py b/bin/lakeroad-portfolio.py
@@ -74,6 +74,12 @@
     default=[],
     action="append",
 )
+parser.add_argument(
+    "--stp", action=argparse.BooleanOptionalAction, help="Use stp.", default=False
+)
+parser.add_argument(
+    "--yices", action=argparse.BooleanOptionalAction, help="Use yices2.", default=False
+)
 parser.add_argument(
     "--boolector",
     action=argparse.BooleanOptionalAction,
@@ -135,6 +141,10 @@ def _parse_flag_set(flag_set: str) -> List[str]:
         )
 if args.boolector:
     solvers_and_flag_sets.append(("boolector", []))
+if args.stp:
+    solvers_and_flag_sets.append(("stp", []))
+if args.yices:
+    solvers_and_flag_sets.append(("yices", []))
 assert solvers_and_flag_sets != [], "Must specify at least one solver."
 
 

diff --git a/bin/main.rkt b/bin/main.rkt
@@ -28,6 +28,8 @@
          rosette/solver/smt/cvc5
          rosette/solver/smt/cvc4
          rosette/solver/smt/bitwuzla
+         rosette/solver/smt/stp
+         rosette/solver/smt/yices
          "../racket/signal.rkt"
          "../racket/btor.rkt"
          racket/sandbox)
@@ -182,6 +184,8 @@
   ["cvc4" (current-solver (cvc4 #:logic 'QF_BV #:options (solver-flags)))]
   ["bitwuzla" (current-solver (bitwuzla #:logic 'QF_BV #:options (solver-flags)))]
   ["boolector" (current-solver (boolector #:logic 'QF_BV #:options (solver-flags)))]
+  ["stp" (current-solver (stp #:logic 'QF_BV #:options (solver-flags)))]
+  ["yices" (current-solver (yices #:logic 'QF_BV #:options (solver-flags)))]
   [_ (error (format "Unknown solver: ~a" (solver)))])
 
 ;;; Parse instruction. Returns a Racket function in the format currently expected by synthesis:

diff --git a/integration_tests/lakeroad/xilinx_addmulsub_3_stage_unsigned_18_bit.sv b/integration_tests/lakeroad/xilinx_addmulsub_3_stage_unsigned_18_bit.sv
@@ -1,6 +1,6 @@
 // RUN: outfile=$(mktemp)
 // RUN: (racket $LAKEROAD_DIR/bin/main.rkt \
-// RUN:  --solver cvc5 \
+// RUN:  --solver stp \
 // RUN:  --verilog-module-filepath %s \
 // RUN:  --architecture xilinx-ultrascale-plus \
 // RUN:  --template dsp \
@@ -19,33 +19,6 @@
 // RUN:  > $outfile \
 // RUN:  2>&1 
 // RUN: FileCheck %s < $outfile
-// if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
-//   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
-//   exit 0; \
-// else \
-//   python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
-//    --use_random_intermediate_inputs \
-//    --seed=23 \
-//    --max_num_tests=10000 \
-//    --verilog_filepath $outfile \
-//    --verilog_filepath %s \
-//    --clock_name clk \
-//    --initiation_interval 3 \
-//    --output_signal_name out \
-//    --input_signal a:18 \
-//    --input_signal b:18 \
-//    --input_signal c:18 \
-//    --input_signal d:18 \
-//    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
-//    --verilator_extra_arg='-DXIL_XECLIB' \
-//    --verilator_extra_arg='-Wno-UNOPTFLAT' \
-//    --verilator_extra_arg='-Wno-LATCH' \
-//    --verilator_extra_arg='-Wno-WIDTH' \
-//    --verilator_extra_arg='-Wno-STMTDLY' \
-//    --verilator_extra_arg='-Wno-CASEX' \
-//    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
-//    --verilator_extra_arg='-Wno-PINMISSING'; \
-// fi
 
 (* use_dsp = "yes" *) module top(
 	input  [17:0] a,
@@ -68,4 +41,4 @@
 	assign out = stage2;
 endmodule
 
-// CHECK: Synthesis Timeout
+// CHECK: Synthesis failed
diff --git a/integration_tests/lakeroad/xilinx_muladd_0_stage_unsigned_13_bit.sv b/integration_tests/lakeroad/xilinx_muladd_0_stage_unsigned_13_bit.sv
@@ -1,6 +1,6 @@
 // RUN: outfile=$(mktemp)
-// RUN: (racket $LAKEROAD_DIR/bin/main.rkt \
-// RUN:  --solver cvc5 \
+// RUN: racket $LAKEROAD_DIR/bin/main.rkt \
+// RUN:  --solver stp \
 // RUN:  --verilog-module-filepath %s \
 // RUN:  --architecture xilinx-ultrascale-plus \
 // RUN:  --template dsp \
@@ -13,35 +13,8 @@
 // RUN:  --input-signal b:13 \
 // RUN:  --input-signal c:13 \
 // RUN:  --timeout 90 \
-// RUN:  || true) \
-// RUN:  > $outfile \
-// RUN:  2>&1
-// FileCheck %s < $outfile
-// if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
-//   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
-//   exit 0; \
-// else \
-//   python $LAKEROAD_DIR/bin/simulate_with_verilator.py \
-//    --use_random_intermediate_inputs \
-//    --seed=23 \
-//    --max_num_tests=10000 \
-//    --verilog_filepath $outfile \
-//    --verilog_filepath %s \
-//    --initiation_interval 0 \
-//    --output_signal_name out \
-//    --input_signal a:13 \
-//    --input_signal b:13 \
-//    --input_signal c:13 \
-//    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
-//    --verilator_extra_arg='-DXIL_XECLIB' \
-//    --verilator_extra_arg='-Wno-UNOPTFLAT' \
-//    --verilator_extra_arg='-Wno-LATCH' \
-//    --verilator_extra_arg='-Wno-WIDTH' \
-//    --verilator_extra_arg='-Wno-STMTDLY' \
-//    --verilator_extra_arg='-Wno-CASEX' \
-//    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
-//    --verilator_extra_arg='-Wno-PINMISSING'; \
-// fi
+// RUN:  > $outfile
+// RUN: FileCheck %s < $outfile
 
 (* use_dsp = "yes" *) module top(
 	input  [12:0] a,
@@ -53,4 +26,5 @@
 	assign out = (a * b) + c;
 endmodule
 
-// CHECK: Synthesis Timeout
+// CHECK: module top(a, b, c, out);
+
diff --git a/integration_tests/lakeroad/xilinx_muladd_3_stage_signed_18_bit.sv b/integration_tests/lakeroad/xilinx_muladd_3_stage_signed_18_bit.sv
@@ -1,6 +1,6 @@
 // RUN: outfile=$(mktemp)
 // RUN: (racket $LAKEROAD_DIR/bin/main.rkt \
-// RUN:  --solver cvc5 \
+// RUN:  --solver stp \
 // RUN:  --verilog-module-filepath %s \
 // RUN:  --architecture xilinx-ultrascale-plus \
 // RUN:  --template dsp \
@@ -19,32 +19,6 @@
 // RUN:  > $outfile \
 // RUN:  2>&1
 // RUN: FileCheck %s < $outfile
-// if [ -z ${LAKEROAD_PRIVATE_DIR+x} ]; then \
-//   echo "Warning: LAKEROAD_PRIVATE_DIR is not set. Skipping simulation."; \
-//   exit 0; \
-// else \
-//   python3 $LAKEROAD_DIR/bin/simulate_with_verilator.py \
-//    --test_module_name test_module \
-//    --ground_truth_module_name top \
-//    --max_num_tests=10000 \
-//    --verilog_filepath $outfile \
-//    --verilog_filepath %s \
-//    --clock_name clk \
-//    --initiation_interval 3 \
-//    --output_signal out:18 \
-//    --input_signal a:18 \
-//    --input_signal b:18 \
-//    --input_signal c:18 \
-//    --verilator_include_dir "$LAKEROAD_PRIVATE_DIR/DSP48E2/" \
-//    --verilator_extra_arg='-DXIL_XECLIB' \
-//    --verilator_extra_arg='-Wno-UNOPTFLAT' \
-//    --verilator_extra_arg='-Wno-LATCH' \
-//    --verilator_extra_arg='-Wno-WIDTH' \
-//    --verilator_extra_arg='-Wno-STMTDLY' \
-//    --verilator_extra_arg='-Wno-CASEX' \
-//    --verilator_extra_arg='-Wno-TIMESCALEMOD' \
-//    --verilator_extra_arg='-Wno-PINMISSING'; \
-// fi
 
 (* use_dsp = "yes" *) module top(
     input signed [17:0] a,
@@ -67,4 +41,4 @@
   assign out = stage2;
 endmodule
 
-// CHECK: Synthesis Timeout
+// CHECK: Synthesis failed