Skip to content

Commit

Permalink
updated main.rkt to support selective generation of rosette's output-… (
Browse files Browse the repository at this point in the history
#460)

…smt feature from the commandline

(PR in response to [@gussmith23's
issue](#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
```
  • Loading branch information
cknizek authored Aug 31, 2024
1 parent 1ccfb09 commit 5050fc6
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions bin/main.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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."
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 5050fc6

Please sign in to comment.