Merge 51560b0bf6 into c21cd300a0

backends/functional/smtlib_rosette.cc

@@ -188,12 +188,14 @@ struct SmtrModule {
 	Functional::IR ir;
 	SmtrScope scope;
 	std::string name;
-	
+	std::optional<std::string> input_helper_name;
+	std::optional<std::string> output_helper_name;
+
 	SmtrStruct input_struct;
 	SmtrStruct output_struct;
 	SmtrStruct state_struct;
 
-	SmtrModule(Module *module)
+	SmtrModule(Module *module, bool assoc_list_helpers)
 		: ir(Functional::IR::from_module(module))
 		, scope()
 		, name(scope.unique_name(module->name))
@@ -202,6 +204,12 @@ struct SmtrModule {
 		, state_struct(scope.unique_name(module->name.str() + "_State"), scope)
 	{
 		scope.reserve(name + "_initial");
+		if (assoc_list_helpers) {
+			input_helper_name = scope.unique_name(module->name.str() + "_inputs_helper");
+			scope.reserve(*input_helper_name);
+			output_helper_name = scope.unique_name(module->name.str() + "_outputs_helper");
+			scope.reserve(*output_helper_name);
+		}
 		for (auto input : ir.inputs())
 			input_struct.insert(input->name, input->sort);
 		for (auto output : ir.outputs())
@@ -257,6 +265,43 @@ struct SmtrModule {
 		w.pop();
 	}
 
+	void write_assoc_list_helpers(SExprWriter &w)
+	{
+		// Input struct keyword-based constructor.
+		w.push();
+		w.open(list("define"));
+		const auto inputs_name = "inputs";
+		w.open(list(*input_helper_name, inputs_name));
+		w.close();
+		w.open(list(input_struct.name));
+		for (auto input : ir.inputs()) {
+			w.push();
+			w.open(list("let"));
+			w.push();
+			w.open(list());
+			w.open(list("assoc-result"));
+			w << list("assoc", "\"" + RTLIL::unescape_id(input->name) + "\"", inputs_name);
+			w.pop();
+			w.open(list("if", "assoc-result"));
+			w << list("cdr", "assoc-result");
+			w.open(list("begin"));
+			w << list("fprintf", list("current-error-port"), "\"%s not found in inputs\"");
+			w << "'not-found";
+			w.pop();
+		}
+		w.pop();
+		// Output struct keyword-based destructor.
+		w.push();
+		w.open(list("define"));
+		const auto outputs_name = "outputs";
+		w << list(*output_helper_name, outputs_name);
+		w.open(list("list"));
+		for (auto output : ir.outputs()) {
+			w << list("cons", "\"" + RTLIL::unescape_id(output->name) + "\"", output_struct.access("outputs", output->name));
+		}
+		w.pop();
+	}
+
 	void write(std::ostream &out)
 	{    
 		SExprWriter w(out);
@@ -265,6 +310,12 @@ struct SmtrModule {
 		output_struct.write_definition(w);
 		state_struct.write_definition(w);
 
+		if (input_helper_name) {
+			if (!output_helper_name)
+				log_error("if keyword helpers are enabled, both input and output helper names are expected");
+			write_assoc_list_helpers(w);
+		}
+
 		write_eval(w);
 		write_initial(w);
 	}
@@ -282,12 +333,16 @@ struct FunctionalSmtrBackend : public Backend {
 		log("\n");
 		log("    -provides\n");
 		log("        include 'provide' statement(s) for loading output as a module\n");
+		log("    -assoc-list-helpers\n");
+		log("        provide helper functions which convert inputs/outputs from/to association lists\n");
+		log("        \n");
 		log("\n");
 	}
 
 	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		auto provides = false;
+		auto assoc_list_helpers = false;
 
 		log_header(design, "Executing Functional Rosette Backend.\n");
 
@@ -296,6 +351,8 @@ struct FunctionalSmtrBackend : public Backend {
 		{
 			if (args[argidx] == "-provides")
 				provides = true;
+			else if (args[argidx] == "-assoc-list-helpers")
+				assoc_list_helpers = true;
 			else
 				break;
 		}
@@ -308,7 +365,7 @@ struct FunctionalSmtrBackend : public Backend {
 
 		for (auto module : design->selected_modules()) {
 			log("Processing module `%s`.\n", module->name.c_str());
-			SmtrModule smtr(module);
+			SmtrModule smtr(module, assoc_list_helpers);
 			smtr.write(*f);
 		}
 	}

tests/functional/run-test.sh

@@ -1,2 +1,2 @@
 #!/usr/bin/env bash
-pytest -v -m "not smt and not rkt" "$@"
+pytest -v "$@"

tests/functional/simulate_rosette.py

@@ -0,0 +1 @@
+"""Python utilities for simulating Rosette code."""

tests/functional/simulate_rosette.rkt

@@ -0,0 +1,104 @@
+; Utilities for simulating Rosette programs.
+#lang racket/base
+
+(provide simulate-rosette)
+
+(require (only-in rosette bv)
+         racket/match
+         racket/list)
+
+; Inputs:
+; - function: The function for the module to simulate. This should be a Rosette function generated by
+;   Yosys's `write_fuctional_rosette` backend.
+; - input-helper, output-helper: association-list-based helpers for input and output struct, generated
+;   by Yosys's `write_fuctional_rosette` backend with `-assoc-list-helpers` enabled.
+; - initial-state: The initial state of the module, as generated by Yosys's `write_fuctional_rosette`
+;   backend.
+(define (simulate-rosette #:function function
+                          #:input-helper input-helper
+                          #:output-helper output-helper
+                          #:initial-state initial-state
+                          #:inputs inputs
+                          #:outputs outputs)
+  (error "TODO: Implement simulate-rosette function"))
+
+; Inputs:
+; - config: Association list mapping input name (string) to a configuration value, which is one of the
+;   following:
+;   - 'exhaustive: The input should be exhaustively tested.
+;   - <integer>: The input should be tested with this many random inputs. When the input is not
+;     present in the config, it defaults to 'exhaustive.
+; -
+(define (generate-inputs #:input-helper input-helper
+                         #:num-inputs num-inputs
+                         #:config config
+                         #:inputs inputs)
+  ; Fill out missing vallues in the config with 'exhaustive.
+  (define config
+    (map (λ (input)
+           (let ([found (assoc (car input) config)]) (or found (cons (car input) 'exhaustive))))
+         inputs))
+
+  ; ; Generate the inputs.
+  ; (define generated-inputs
+  ;   (map (λ (input)
+  ;          (let ([input-name (car input)] [input-bitwidth (cdr input)])
+  ;            (cond
+  ;              [(equal? 'exhaustive (cdr (assoc input-name config))) (list input-name 'exhaustive)]
+  ;              [(number? (cdr (assoc input-name config)))
+  ;               (list input-name (make-random-input input-type (cdr (assoc input-name config))))]
+  ;              [else (error "Invalid configuration for input" input-name)])))
+  ;        inputs))
+
+  (error "TODO"))
+
+; Helper function: for a given input name, bitwidth, and configuration, generate a list of inputs.
+; Output: List of Rosette bitvector values for the input.
+(define (generate-inputs-for-one input-name bitwidth config)
+  (cond
+    ; If the configuration is 'exhaustive, or if they request a number of inputs that is greater than
+    ; or equal to the number of possible values for the bitwidth, generate all possible inputs.
+    [(or (equal? config 'exhaustive) (and (number? config) (>= config (expt 2 bitwidth))))
+     (for/list ([n (range (expt 2 bitwidth))])
+       (bv n bitwidth))]
+    [(and (number? config) (positive? config))
+     (map (λ (_) (bv (random (expt 2 bitwidth)) bitwidth)) (range config))]
+    [else (error (format "Invalid configuration ~a for input ~a" config input-name))]))
+
+; This is what gets executed when the script is run.
+(module main racket/base
+  (require racket/cmdline))
+
+(module+ test
+  (require rackunit)
+  (test-case "generate-inputs-for-one"
+    (check-equal? (generate-inputs-for-one "input1" 4 'exhaustive)
+                  (list (bv 0 4)
+                        (bv 1 4)
+                        (bv 2 4)
+                        (bv 3 4)
+                        (bv 4 4)
+                        (bv 5 4)
+                        (bv 6 4)
+                        (bv 7 4)
+                        (bv 8 4)
+                        (bv 9 4)
+                        (bv 10 4)
+                        (bv 11 4)
+                        (bv 12 4)
+                        (bv 13 4)
+                        (bv 14 4)
+                        (bv 15 4)))
+
+    ; Requesting fewer inputs than the number of possible values for the bitwidth.
+    (check-equal? (length (generate-inputs-for-one "input2" 3 5)) 5)
+
+    ; Requesting more inputs than the number of possible values for the bitwidth.
+    (check-equal? (generate-inputs-for-one "input3" 2 5) (list (bv 0 2) (bv 1 2) (bv 2 2) (bv 3 2)))
+
+    ; Requesting equal number of inputs as the number of possible values for the bitwidth.
+    (check-equal? (generate-inputs-for-one "input4" 2 4) (list (bv 0 2) (bv 1 2) (bv 2 2) (bv 3 2)))
+
+    ; Requesting invalid configuration should raise an error.
+    (check-exn exn:fail? (λ () (generate-inputs-for-one "input5" 2 'invalid-config)))
+    (check-exn exn:fail? (λ () (generate-inputs-for-one "input5" 2 bytes->string/latin-1)))))