From 5050fc6597e49095bc56c368c723233177037df0 Mon Sep 17 00:00:00 2001
From: cknizek <87683288+cknizek@users.noreply.github.com>
Date: Sat, 31 Aug 2024 19:46:09 +0700
Subject: [PATCH] =?UTF-8?q?updated=20main.rkt=20to=20support=20selective?=
 =?UTF-8?q?=20generation=20of=20rosette's=20output-=E2=80=A6=20(#460)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

…smt feature from the commandline

(PR in response to [@gussmith23's
issue](https://github.com/uwsampl/lakeroad/issues/453))

### What this change does:
This change modifies `main.rkt` to support the command line flag
`--output-smt-path "path"`. The specified path will be used as the
output to Rosette's `output-smt` feature.

The path you specify will become a folder, as there may be many SMT
output files generated and placed in the selected path.

### How this change does it:
It adds a new parameter, `output-smt-path` (initially set to `#f`) to
`main.rkt`.

If `output-smt-path` becomes no longer equal to `#f` (i.e. it has been
assigned in the commandline arguments to become something), the SMT
output feature of Rosette will be activated. The output will be directed
to the path specified.

### How to use this change (see line 2 of the below code block):
```
// RUN: racket $LAKEROAD_DIR/bin/main.rkt \
// RUN:  --output-smt-path "example_test_using_include_smt_output_test" \
// RUN:  --solver bitwuzla \
// RUN:  --verilog-module-filepath %s \
// RUN:  --architecture xilinx-ultrascale-plus \
// RUN:  --template dsp \
// RUN:  --out-format verilog \
// RUN:  --top-module-name top \
// RUN:  --verilog-module-out-signal out:11 \
// RUN:  --pipeline-depth 1 \
// RUN:  --clock-name clk \
// RUN:  --module-name out \
// RUN:  --input-signal a:11 \
// RUN:  --input-signal b:11 \
// RUN:  --input-signal c:11 \
// RUN:  --input-signal d:11 \
// RUN:  --extra-cycles 3 \
// RUN:  --timeout 120 \
// RUN: | FileCheck %s
```
---
 bin/main.rkt | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/bin/main.rkt b/bin/main.rkt
index 7a062c5d..e1d36a46 100755
--- a/bin/main.rkt
+++ b/bin/main.rkt
@@ -88,6 +88,7 @@
 (define cvc4-path (make-parameter #f))
 (define boolector-path (make-parameter #f))
 (define yosys-log-filepath (make-parameter #f))
+(define output-smt-path (make-parameter #f))
 
 (command-line
  #:program "lakeroad"
@@ -128,6 +129,7 @@
     (when (not (file-exists? v))
       (error (format "File ~a does not exist." v)))
     (verilog-module-filepath v))]
+ ["--output-smt-path" v "Specify the output of the SMT solver to a directory." (output-smt-path v)]
  ["--top-module-name"
   v
   "Top module name if --verilog-module-filepath is specified."
@@ -274,6 +276,9 @@
        (list (cons ',(string->symbol (verilog-module-out-signal)) (bv->signal ,body)))))
   (eval out-fn ns))
 
+(when (output-smt-path)
+  (output-smt (output-smt-path)))
+
 ;;; The bitvector expression we're trying to synthesize.
 (define bv-expr
   (cond