Enable rosette's output-smt via a command-line option
#453
Labels
good first issue
Good for newcomers
Comments
cknizek
added a commit
that referenced
this issue
Aug 31, 2024
#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 ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I often find myself needing to debug the SMT queries Rosette produces. I currently have to add in a line that calls
(output-smt)intomain.rktevery time. Would be good to just allow this to be enabled via command line. Would also be good to have the evaluation produce all of these SMT files.The text was updated successfully, but these errors were encountered: