From c3ec67a5a161b701374cbd2bcd234b4b0e8f6efa Mon Sep 17 00:00:00 2001
From: Gus Smith <guscomps@gmail.com>
Date: Thu, 14 Dec 2023 15:06:41 -0800
Subject: [PATCH] Test uses STP

---
 .../xilinx_muladd_3_stage_signed_18_bit.sv    | 30 ++-----------------
 1 file changed, 2 insertions(+), 28 deletions(-)

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
index d18906f0..e13fbfdb 100644
--- 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