Better port specifications

README.md

@@ -152,3 +152,10 @@ TODO(@gussmith23): Find better cross-platform regex. I thought Perl might be the
 Lakeroad is usable via a Yosys plugin, which can be built separately and loaded directly into your existing Yosys installation. The plugin is located in [./yosys-plugin/](./yosys-plugin/) and can be built using the Makefile in that directory. The plugin can be loaded into Yosys using Yosys's `-m` option, e.g. `yosys -m lakeroad.so ...`. An example of this can be seen in [this integration test.](./integration_tests/lakeroad/xilinx_muladd_0_stage_signed_8_bit_yosys_plugin.sv)
 
 Note: the Lakeroad plugin needs to be built in the same environment (i.e. same glibc version) as the Yosys executable it's being loaded into. This can be an issue e.g. when using the Yosys executable in `oss-cad-suite`. The easiest way to prevent this is to build Yosys yourself using their directions.
+
+## Debugging for Developers
+
+Debugging Racket and Rosette can be very frustrating. Here are notes that may be useful.
+
+- Use errortrace in Racket.
+- Use the Rosette symbolic debugger `symtrace`.

bin/main.rkt

@@ -79,6 +79,19 @@
 ;;; inputs is an association list mapping input name to an integer bitwidth.
 (define inputs (make-parameter '()))
 (define solver (make-parameter "bitwuzla"))
+; List of (port-name:string, width:int) pairs.
+(define ports (make-parameter '()))
+(define (parse-dsl expr-str)
+  (define expr (read (open-input-string expr-str)))
+  (define (recursive-helper expr)
+    (match expr
+      [`(extract ,i ,j ,expr) (lr:extract (lr:integer i) (lr:integer j) (recursive-helper expr))]
+      [`(port ,(? symbol? sym) ,width)
+       ; Add port to list of ports, if it's not there.
+       (unless (assoc sym (ports))
+         (ports (append (ports) (list (list (symbol->string sym) width)))))
+       (lr:var (symbol->string sym) width)]))
+  (recursive-helper expr))
 (define extra-cycles (make-parameter 0))
 (define solver-flags (make-parameter (make-hash)))
 (define bitwuzla-path (make-parameter #f))
@@ -211,16 +224,21 @@
  [("--module-name") v "Name given to the module produced." (module-name v)]
  [("--input-signal")
   v
-  "Name of an input signal to the module in the format `<name>:<bw` e.g. `a:8` This flag can be"
-  " specified multiple times. This currently only needs to be specified for sequential synthesis."
-  ;;; Parse --input arg: split <name>:<bw> into name and bw, construct Rosette symbolic input.
-  (let* ([splits (string-split v ":")] [name (first splits)] [bw (string->number (second splits))])
-    (when (not (equal? 2 (length splits)))
-      (error (format "Invalid input signal specification: ~a" v)))
-    (when (assoc name (inputs))
-      (error "Signal " name " already present; did you duplicate an --input?"))
-    (inputs (append (inputs) (list (cons name bw)))))])
+  "Specify an input to the sketch, using a small domain-specific language. Generally, the inputs to"
+  " the sketch will correspond to the input ports of the module you are trying to compile. For"
+  " example, if you were compiling a multiplier module with 8-bit inputs `i0` and `i1` using the `dsp`"
+  " sketch, you would plug the `i0` and `i1` input ports into the `a` and `b` inputs of"
+  " the DSP sketch by specifying `--input-signal 'a:(port i0 8):8' --input-signal 'b:(port i1 8):8'`."
+  (let* ([splits (string-split v ":")]
+         [_ (when (not (equal? 3 (length splits)))
+              (error (format "Invalid input signal specification: ~a" v)))]
+         [id (first splits)]
+         [expr (parse-dsl (second splits))]
+         [bw (string->number (third splits))])
 
+    (when (assoc id (inputs))
+      (error "Signal " id " already present; did you duplicate an --input?"))
+    (inputs (append (inputs) (list (list id expr bw)))))])
 ;;; Set solver.
 (match (solver)
   ["cvc5" (current-solver (cvc5 #:path (cvc5-path) #:logic 'QF_BV #:options (solver-flags)))]
@@ -393,7 +411,7 @@
 
 (define sketch-inputs
   (make-sketch-inputs #:output-width output-bitwidth
-                      #:data (map (λ (p) (cons (lr:var (car p) (cdr p)) (cdr p))) (inputs))
+                      #:data (map (lambda (p) (cons (first p) (cons (second p) (third p)))) (inputs))
                       #:clk (if (clock-name) (cons (lr:var (clock-name) 1) 1) #f)
                       #:rst (if (reset-name) (cons (lr:var (reset-name) 1) 1) #f)))
 (define sketch (first (sketch-generator architecture-description sketch-inputs)))
@@ -415,16 +433,16 @@
             [input-values
              (map (λ (p)
                     (match p
-                      [(cons name bw)
+                      [(list name bw)
                        (cons name (bv->signal (constant (list "main.rkt" name) (bitvector bw))))]))
-                  (inputs))]
+                  (ports))]
 
             ;;; The same environments, but with symbolic values
             [make-intermediate-inputs
              (lambda (inputs iter)
                (map (λ (p)
                       (match p
-                        [(cons name bw)
+                        [(list name bw)
                          (cons name (bv->signal (constant (list name "iter" iter) (bitvector bw))))]))
                     inputs))]
 
@@ -436,14 +454,14 @@
             ;;; First, we tick the clock with the inputs set to their input values.
             [envs (append (list (cons (cons (clock-name) (bv->signal (bv 0 1))) input-values)
                                 (cons (cons (clock-name) (bv->signal (bv 1 1)))
-                                      (make-intermediate-inputs (inputs) 0)))
+                                      (make-intermediate-inputs (ports) 0)))
                           ;;; then, we tick the clock with the inputs set to symbolic values.
                           (apply append
                                  (map (lambda (iter)
                                         (list (cons (cons (clock-name) (bv->signal (bv 0 1)))
-                                                    (make-intermediate-inputs (inputs) iter))
+                                                    (make-intermediate-inputs (ports) iter))
                                               (cons (cons (clock-name) (bv->signal (bv 1 1)))
-                                                    (make-intermediate-inputs (inputs) iter))))
+                                                    (make-intermediate-inputs (ports) iter))))
                                       (range 1 (+ (pipeline-depth) (extra-cycles))))))]
             ;;; If there's a reset signal, set it to 0 in all envs.
             [envs (if (reset-name)
@@ -496,10 +514,10 @@
      (define envs
        (list (append (map (λ (p)
                             (match p
-                              [(cons name bw)
+                              [(list name bw)
                                (cons name
                                      (bv->signal (constant (list "main.rkt" name) (bitvector bw))))]))
-                          (inputs))
+                          (ports))
                      ; If there's a clock, hardcode it to 0.
                      (if (clock-name) (list (cons (clock-name) (bv->signal (bv 0 1)))) (list)))))
      (define input-symbolic-constants (symbolics envs))

integration_tests/lakeroad/addmulor_3_stage_unsigneds_9_bit.v

@@ -11,10 +11,10 @@
 // RUN:  --pipeline-depth 3 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:9 \
-// RUN:  --input-signal b:9 \
-// RUN:  --input-signal c:9 \
-// RUN:  --input-signal d:9 \
+// RUN:  --input-signal 'a:(port a 9):9' \
+// RUN:  --input-signal 'b:(port b 9):9' \
+// RUN:  --input-signal 'c:(port c 9):9' \
+// RUN:  --input-signal 'd:(port d 9):9' \
 // RUN:  --timeout 90 \
 // RUN:  --extra-cycles 3 \
 // RUN: || true) \

integration_tests/lakeroad/combinational_multiplier_lattice.v

@@ -7,8 +7,8 @@
 // RUN:  --top-module-name top \
 // RUN:  --verilog-module-out-signal p:16 \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
 // RUN:  --timeout 120 \
 // RUN: | FileCheck %s
 

integration_tests/lakeroad/combinational_multiplier_xilinx.v

@@ -8,8 +8,8 @@
 // RUN:  --verilog-module-out-signal p:16 \
 // RUN:  --pipeline-depth 0 \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
 // RUN:  --timeout 90 \
 // RUN: | FileCheck %s
 

integration_tests/lakeroad/example_test_using_include.v

@@ -9,8 +9,8 @@
 // RUN:  --verilog-module-out-signal p:16 \
 // RUN:  --pipeline-depth 0 \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
 // RUN:  --timeout 90 \
 // RUN: > $outfile
 // RUN: FileCheck %s < $outfile

integration_tests/lakeroad/intel_cyclone10lp_mul_0_stage_unsigned_18_bit.v

@@ -8,8 +8,8 @@
 // RUN:  --top-module-name top \
 // RUN:  --verilog-module-out-signal p:18 \
 // RUN:  --module-name test_module \
-// RUN:  --input-signal a:18 \
-// RUN:  --input-signal b:18 \
+// RUN:  --input-signal 'a:(port a 18):18' \
+// RUN:  --input-signal 'b:(port b 18):18' \
 // RUN:  --timeout 120 \
 // RUN:  > $outfile
 // RUN: FileCheck %s < $outfile

integration_tests/lakeroad/intel_cyclone10lp_mul_1_stage_unsigned_18_bit.v

@@ -8,8 +8,8 @@
 // RUN:  --top-module-name top \
 // RUN:  --verilog-module-out-signal p:18 \
 // RUN:  --module-name test_module \
-// RUN:  --input-signal a:18 \
-// RUN:  --input-signal b:18 \
+// RUN:  --input-signal 'a:(port a 18):18' \
+// RUN:  --input-signal 'b:(port b 18):18' \
 // RUN:  --pipeline-depth 1 \
 // RUN:  --clock-name clk \
 // RUN:  --timeout 60 \

integration_tests/lakeroad/intel_cyclone10lp_mul_2_stage_unsigned_18_bit.v

@@ -8,8 +8,8 @@
 // RUN:  --top-module-name top \
 // RUN:  --verilog-module-out-signal p:18 \
 // RUN:  --module-name test_module \
-// RUN:  --input-signal a:18 \
-// RUN:  --input-signal b:18 \
+// RUN:  --input-signal 'a:(port a 18):18' \
+// RUN:  --input-signal 'b:(port b 18):18' \
 // RUN:  --pipeline-depth 2 \
 // RUN:  --clock-name clk \
 // RUN:  --timeout 60 \

integration_tests/lakeroad/lattice_mult_2_stage_signed_8_bit.sv

@@ -10,8 +10,8 @@
 // RUN:  --pipeline-depth 2 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name test_module \
-// RUN:  --input-signal a:8 \
-// RUN:  --input-signal b:8 \
+// RUN:  --input-signal 'a:(port a 8):8' \
+// RUN:  --input-signal 'b:(port b 8):8' \
 // RUN:  --extra-cycles 3 \
 // RUN:  --timeout 120 \
 // RUN:  > $outfile

integration_tests/lakeroad/mul16_yosys_techmap.txt

@@ -5,8 +5,8 @@ RUN:  --architecture xilinx-ultrascale-plus \
 RUN:  --template dsp \
 RUN:  --out-format yosys-techmap \
 RUN:  --module-name out \
-RUN:  --input-signal a:16 \
-RUN:  --input-signal b:16 \
+RUN:  --input-signal 'a:(port a 16):16' \
+RUN:  --input-signal 'b:(port b 16):16' \
 RUN:  --verilog-module-out-signal p:16 \
 RUN:  --timeout 90 \
 RUN:  || true) \

integration_tests/lakeroad/one_stage_add_mul_add_signed_11_bit_xilinx.sv

@@ -9,10 +9,10 @@
 // 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:  --input-signal 'a:(port a 11):11' \
+// RUN:  --input-signal 'b:(port b 11):11' \
+// RUN:  --input-signal 'c:(port c 11):11' \
+// RUN:  --input-signal 'd:(port d 11):11' \
 // RUN:  --extra-cycles 3 \
 // RUN:  --timeout 120 \
 // RUN: | FileCheck %s

integration_tests/lakeroad/one_stage_add_mul_add_signed_12_bit_xilinx.sv

@@ -9,10 +9,10 @@
 // RUN:  --pipeline-depth 1 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:12 \
-// RUN:  --input-signal b:12 \
-// RUN:  --input-signal c:12 \
-// RUN:  --input-signal d:12 \
+// RUN:  --input-signal 'a:(port a 12):12' \
+// RUN:  --input-signal 'b:(port b 12):12' \
+// RUN:  --input-signal 'c:(port c 12):12' \
+// RUN:  --input-signal 'd:(port d 12):12' \
 // RUN:  --extra-cycles 3 \
 // RUN:  --timeout 120 \
 // RUN: | FileCheck %s

integration_tests/lakeroad/one_stage_add_mul_add_signed_18_bit_xilinx.sv

@@ -10,10 +10,10 @@
 // RUN:  --pipeline-depth 1 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name test_module \
-// RUN:  --input-signal a:18 \
-// RUN:  --input-signal b:18 \
-// RUN:  --input-signal c:18 \
-// RUN:  --input-signal d:18 \
+// RUN:  --input-signal 'a:(port a 18):18' \
+// RUN:  --input-signal 'b:(port b 18):18' \
+// RUN:  --input-signal 'c:(port c 18):18' \
+// RUN:  --input-signal 'd:(port d 18):18' \
 // RUN:  --extra-cycles 1 \
 // RUN:  --timeout 120 \
 // RUN: > $outfile

integration_tests/lakeroad/one_stage_mul_or_lattice.v

@@ -10,9 +10,9 @@
 // RUN:  --pipeline-depth 1 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name test_module \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
-// RUN:  --input-signal c:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
+// RUN:  --input-signal 'c:(port c 16):16' \
 // RUN:  --extra-cycles 3 \
 // RUN:  --timeout 120 \
 // RUN:  > $outfile

integration_tests/lakeroad/one_stage_multiplier_lattice.v

@@ -10,8 +10,8 @@
 // RUN:  --pipeline-depth 1 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name test_module \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
 // RUN:  --extra-cycles 3 \
 // RUN:  --timeout 120 \
 // RUN:  > $outfile

integration_tests/lakeroad/pipeline_depth_0_with_clk_test.v

@@ -8,13 +8,13 @@
 // RUN:  --verilog-module-out-signal o:16 \
 // RUN:  --pipeline-depth 0 \
 // RUN:  --module-name out \
-// RUN:  --input-signal i:16 \
+// RUN:  --input-signal 'c:(port i 16):16' \
 // RUN:  --clock-name clk \
 // RUN:  --timeout 90 \
 // RUN: | FileCheck %s
 
 module simple(input clk, input [15:0] i, output [15:0] o);
-  assign o = a;
+  assign o = i;
 endmodule
 
 // CHECK: module out(clk, i, o);

integration_tests/lakeroad/three_stage_mul_and_lattice.v

@@ -9,9 +9,9 @@
 // RUN:  --pipeline-depth 3 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
-// RUN:  --input-signal c:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
+// RUN:  --input-signal 'c:(port c 16):16' \
 // RUN:  --extra-cycles 3 \
 // RUN:  --timeout 120 \
 // RUN: || true) \

integration_tests/lakeroad/three_stage_multiplier_lattice.v

@@ -9,8 +9,8 @@
 // RUN:  --pipeline-depth 3 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
 // RUN:  --extra-cycles 3 \
 // RUN:  --timeout 120 \
 // RUN: | FileCheck %s

integration_tests/lakeroad/three_stage_multiplier_xilinx.v

@@ -9,8 +9,8 @@
 // RUN:  --pipeline-depth 3 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
 // RUN:  --timeout 90 \
 // This one termiates with 2 extra cycles, but not 3.
 // RUN:  --extra-cycles 2 \

integration_tests/lakeroad/two_stage_mul_and_lattice.v

@@ -10,9 +10,9 @@
 // RUN:  --pipeline-depth 2 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name test_module \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
-// RUN:  --input-signal c:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
+// RUN:  --input-signal 'c:(port c 16):16' \
 // RUN:  --timeout 90 \
 // RUN:  --extra-cycles 3 \
 // RUN:  > $outfile \

integration_tests/lakeroad/two_stage_multiplier_xilinx.v

@@ -9,8 +9,8 @@
 // RUN:  --pipeline-depth 2 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:16 \
-// RUN:  --input-signal b:16 \
+// RUN:  --input-signal 'a:(port a 16):16' \
+// RUN:  --input-signal 'b:(port b 16):16' \
 // RUN:  --extra-cycles 1 \
 // RUN:  --timeout 120 \
 // RUN: | FileCheck %s

integration_tests/lakeroad/xilinx-7-series/7_series_addmuladd_1_stage_signed_11_bit.sv

@@ -10,10 +10,10 @@
 // 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:  --input-signal 'a:(port a 11):11' \
+// RUN:  --input-signal 'b:(port b 11):11' \
+// RUN:  --input-signal 'c:(port c 11):11' \
+// RUN:  --input-signal 'd:(port d 11):11' \
 // RUN:  --timeout 120 \
 // RUN:  --extra-cycles 3 \
 // RUN:  > $outfile

integration_tests/lakeroad/xilinx-7-series/7_series_addmuladd_1_stage_signed_9_bit.sv

@@ -10,10 +10,10 @@
 // RUN:  --pipeline-depth 1 \
 // RUN:  --clock-name clk \
 // RUN:  --module-name out \
-// RUN:  --input-signal a:9 \
-// RUN:  --input-signal b:9 \
-// RUN:  --input-signal c:9 \
-// RUN:  --input-signal d:9 \
+// RUN:  --input-signal 'a:(port a 9):9' \
+// RUN:  --input-signal 'b:(port b 9):9' \
+// RUN:  --input-signal 'c:(port c 9):9' \
+// RUN:  --input-signal 'd:(port d 9):9' \
 // RUN:  --extra-cycles 3 \
 // RUN:  --timeout 120 \
 // RUN: > $outfile