From fd5918c811c701e82ba56d1040cd2acf327193f4 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Sat, 17 May 2025 14:10:23 -0700 Subject: [PATCH 01/11] get_field_names for structs --- backends/functional/smtlib_rosette.cc | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index c9e737d19..786f7b176 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -114,6 +114,13 @@ public: size_t i = field_names.at(name); return list(fields[i].accessor, std::move(record)); } + std::vector get_field_names() + { + std::vector names; + for (auto field : fields) + names.push_back(field.name); + return names; + } }; std::string smt_const(RTLIL::Const const &c) { From 7b4c9c5dcdbbda993751909a653c080f05688d02 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Sat, 17 May 2025 14:12:09 -0700 Subject: [PATCH 02/11] Add optional keyword-based constructor --- backends/functional/smtlib_rosette.cc | 37 ++++++++++++++++++++++++--- 1 file changed, 34 insertions(+), 3 deletions(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index 786f7b176..316878a76 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -195,12 +195,13 @@ struct SmtrModule { Functional::IR ir; SmtrScope scope; std::string name; - + std::optional input_kw_name; + SmtrStruct input_struct; SmtrStruct output_struct; SmtrStruct state_struct; - SmtrModule(Module *module) + SmtrModule(Module *module, bool keyword_constructor) : ir(Functional::IR::from_module(module)) , scope() , name(scope.unique_name(module->name)) @@ -209,6 +210,10 @@ struct SmtrModule { , state_struct(scope.unique_name(module->name.str() + "_State"), scope) { scope.reserve(name + "_initial"); + if (keyword_constructor) { + input_kw_name = scope.unique_name(module->name.str() + "_inputs_kw"); + scope.reserve(*input_kw_name); + } for (auto input : ir.inputs()) input_struct.insert(input->name, input->sort); for (auto output : ir.outputs()) @@ -264,6 +269,22 @@ struct SmtrModule { w.pop(); } + void write_input_kw(SExprWriter &w) + { + w.push(); + w.open(list("define")); + w.open(list(name + "_inputs_kw")); + for (auto name : input_struct.get_field_names()) { + w << "#:" + name << name; + } + w.close(); + w.open(list(input_struct.name)); + for (auto name : input_struct.get_field_names()) { + w << name; + } + w.pop(); + } + void write(std::ostream &out) { SExprWriter w(out); @@ -272,6 +293,10 @@ struct SmtrModule { output_struct.write_definition(w); state_struct.write_definition(w); + if (input_kw_name) { + write_input_kw(w); + } + write_eval(w); write_initial(w); } @@ -289,12 +314,16 @@ struct FunctionalSmtrBackend : public Backend { log("\n"); log(" -provides\n"); log(" include 'provide' statement(s) for loading output as a module\n"); + log(" -keyword-constructor\n"); + log(" provide a function which can construct inputs using keywords\n"); + log(" \n"); log("\n"); } void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override { auto provides = false; + auto keyword_constructor = false; log_header(design, "Executing Functional Rosette Backend.\n"); @@ -303,6 +332,8 @@ struct FunctionalSmtrBackend : public Backend { { if (args[argidx] == "-provides") provides = true; + else if (args[argidx] == "-keyword-constructor") + keyword_constructor = true; else break; } @@ -315,7 +346,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, keyword_constructor); smtr.write(*f); } } From 10b8fdddb40eb0c7f1a273347428bacdf1b2a9ef Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Sat, 17 May 2025 14:39:11 -0700 Subject: [PATCH 03/11] Rename argument --- backends/functional/smtlib_rosette.cc | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index 316878a76..6769d7384 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -201,7 +201,7 @@ struct SmtrModule { SmtrStruct output_struct; SmtrStruct state_struct; - SmtrModule(Module *module, bool keyword_constructor) + SmtrModule(Module *module, bool keyword_helpers) : ir(Functional::IR::from_module(module)) , scope() , name(scope.unique_name(module->name)) @@ -210,7 +210,7 @@ struct SmtrModule { , state_struct(scope.unique_name(module->name.str() + "_State"), scope) { scope.reserve(name + "_initial"); - if (keyword_constructor) { + if (keyword_helpers) { input_kw_name = scope.unique_name(module->name.str() + "_inputs_kw"); scope.reserve(*input_kw_name); } @@ -314,8 +314,8 @@ struct FunctionalSmtrBackend : public Backend { log("\n"); log(" -provides\n"); log(" include 'provide' statement(s) for loading output as a module\n"); - log(" -keyword-constructor\n"); - log(" provide a function which can construct inputs using keywords\n"); + log(" -keyword-helpers\n"); + log(" provide helper functions which can construct/destruct inputs/outputs using keywords\n"); log(" \n"); log("\n"); } @@ -323,7 +323,7 @@ struct FunctionalSmtrBackend : public Backend { void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override { auto provides = false; - auto keyword_constructor = false; + auto keyword_helpers = false; log_header(design, "Executing Functional Rosette Backend.\n"); @@ -332,8 +332,8 @@ struct FunctionalSmtrBackend : public Backend { { if (args[argidx] == "-provides") provides = true; - else if (args[argidx] == "-keyword-constructor") - keyword_constructor = true; + else if (args[argidx] == "-keyword-helpers") + keyword_helpers = true; else break; } @@ -346,7 +346,7 @@ struct FunctionalSmtrBackend : public Backend { for (auto module : design->selected_modules()) { log("Processing module `%s`.\n", module->name.c_str()); - SmtrModule smtr(module, keyword_constructor); + SmtrModule smtr(module, keyword_helpers); smtr.write(*f); } } From 1fdfba2a1afd9a7811c314914c0ee53cc9abff8e Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Sat, 17 May 2025 15:17:29 -0700 Subject: [PATCH 04/11] Add helper for accessing by base name The existing access function isn't useful if we don't have access to the original names of the input/output/state signals. There may be a better way to do this, but it might require restructuring the SmtrStruct. --- backends/functional/smtlib_rosette.cc | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index 6769d7384..82bfd662a 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -114,6 +114,15 @@ public: size_t i = field_names.at(name); return list(fields[i].accessor, std::move(record)); } + SExpr access_by_base_name(SExpr record, std::string base_name) + { + // Find the field by its base name + auto it = std::find_if(fields.begin(), fields.end(), [&](const Field &field) { return field.name == base_name; }); + if (it == fields.end()) { + log_error("Field with base name '%s' not found in struct '%s'.\n", base_name.c_str(), name.c_str()); + } + return list(it->accessor, std::move(record)); + } std::vector get_field_names() { std::vector names; From c1111f125c391bae17fde32c22f2c926395f31cf Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Sat, 17 May 2025 15:19:09 -0700 Subject: [PATCH 05/11] Add output helper as well --- backends/functional/smtlib_rosette.cc | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index 82bfd662a..a59574fcf 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -205,6 +205,7 @@ struct SmtrModule { SmtrScope scope; std::string name; std::optional input_kw_name; + std::optional output_kw_name; SmtrStruct input_struct; SmtrStruct output_struct; @@ -222,6 +223,8 @@ struct SmtrModule { if (keyword_helpers) { input_kw_name = scope.unique_name(module->name.str() + "_inputs_kw"); scope.reserve(*input_kw_name); + output_kw_name = scope.unique_name(module->name.str() + "_outputs_kw"); + scope.reserve(*output_kw_name); } for (auto input : ir.inputs()) input_struct.insert(input->name, input->sort); @@ -278,8 +281,9 @@ struct SmtrModule { w.pop(); } - void write_input_kw(SExprWriter &w) + void write_keyword_helpers(SExprWriter &w) { + // Input struct keyword-based constructor. w.push(); w.open(list("define")); w.open(list(name + "_inputs_kw")); @@ -292,6 +296,18 @@ struct SmtrModule { w << name; } w.pop(); + // Output struct keyword-based destructor. + w.push(); + w.open(list("define")); + w.open(list(name + "_outputs_kw")); + const auto outputs_name = "outputs"; + w << outputs_name; + w.close(); + w.open(list("list")); + for (auto name : output_struct.get_field_names()) { + w << list("cons", "\"" + name + "\"", output_struct.access_by_base_name(outputs_name, name)); + } + w.pop(); } void write(std::ostream &out) @@ -303,7 +319,9 @@ struct SmtrModule { state_struct.write_definition(w); if (input_kw_name) { - write_input_kw(w); + if (!output_kw_name) + log_error("if keyword helpers are enabled, both input and output helper names are expected"); + write_keyword_helpers(w); } write_eval(w); From a55dc801758126378b8b318519996b947a003b70 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Sat, 17 May 2025 16:04:17 -0700 Subject: [PATCH 06/11] Rename parameter --- backends/functional/smtlib_rosette.cc | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index a59574fcf..4dd0fb855 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -211,7 +211,7 @@ struct SmtrModule { SmtrStruct output_struct; SmtrStruct state_struct; - SmtrModule(Module *module, bool keyword_helpers) + SmtrModule(Module *module, bool assoc_list_helpers) : ir(Functional::IR::from_module(module)) , scope() , name(scope.unique_name(module->name)) @@ -220,7 +220,7 @@ struct SmtrModule { , state_struct(scope.unique_name(module->name.str() + "_State"), scope) { scope.reserve(name + "_initial"); - if (keyword_helpers) { + if (assoc_list_helpers) { input_kw_name = scope.unique_name(module->name.str() + "_inputs_kw"); scope.reserve(*input_kw_name); output_kw_name = scope.unique_name(module->name.str() + "_outputs_kw"); @@ -341,8 +341,8 @@ struct FunctionalSmtrBackend : public Backend { log("\n"); log(" -provides\n"); log(" include 'provide' statement(s) for loading output as a module\n"); - log(" -keyword-helpers\n"); - log(" provide helper functions which can construct/destruct inputs/outputs using keywords\n"); + log(" -assoc-list-helpers\n"); + log(" provide helper functions which convert inputs/outputs from/to association lists\n"); log(" \n"); log("\n"); } @@ -350,7 +350,7 @@ struct FunctionalSmtrBackend : public Backend { void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override { auto provides = false; - auto keyword_helpers = false; + auto assoc_list_helpers = false; log_header(design, "Executing Functional Rosette Backend.\n"); @@ -359,8 +359,8 @@ struct FunctionalSmtrBackend : public Backend { { if (args[argidx] == "-provides") provides = true; - else if (args[argidx] == "-keyword-helpers") - keyword_helpers = true; + else if (args[argidx] == "-assoc-list-helpers") + assoc_list_helpers = true; else break; } @@ -373,7 +373,7 @@ struct FunctionalSmtrBackend : public Backend { for (auto module : design->selected_modules()) { log("Processing module `%s`.\n", module->name.c_str()); - SmtrModule smtr(module, keyword_helpers); + SmtrModule smtr(module, assoc_list_helpers); smtr.write(*f); } } From af51097af77375cc0f46facb449e1472a2514aca Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Sun, 18 May 2025 18:01:43 -0700 Subject: [PATCH 07/11] Convert to 'assoc list helpers' --- backends/functional/smtlib_rosette.cc | 44 ++++++++++++++++----------- 1 file changed, 26 insertions(+), 18 deletions(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index 4dd0fb855..ec116f1a2 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -204,8 +204,8 @@ struct SmtrModule { Functional::IR ir; SmtrScope scope; std::string name; - std::optional input_kw_name; - std::optional output_kw_name; + std::optional input_helper_name; + std::optional output_helper_name; SmtrStruct input_struct; SmtrStruct output_struct; @@ -221,10 +221,10 @@ struct SmtrModule { { scope.reserve(name + "_initial"); if (assoc_list_helpers) { - input_kw_name = scope.unique_name(module->name.str() + "_inputs_kw"); - scope.reserve(*input_kw_name); - output_kw_name = scope.unique_name(module->name.str() + "_outputs_kw"); - scope.reserve(*output_kw_name); + 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); @@ -281,28 +281,36 @@ struct SmtrModule { w.pop(); } - void write_keyword_helpers(SExprWriter &w) + void write_assoc_list_helpers(SExprWriter &w) { // Input struct keyword-based constructor. w.push(); w.open(list("define")); - w.open(list(name + "_inputs_kw")); - for (auto name : input_struct.get_field_names()) { - w << "#:" + name << name; - } + const auto inputs_name = "inputs"; + w.open(list(*input_helper_name, inputs_name)); w.close(); w.open(list(input_struct.name)); for (auto name : input_struct.get_field_names()) { - w << name; + w.push(); + w.open(list("let")); + w.push(); + w.open(list()); + w.open(list("assoc-result")); + w << list("assoc", "\"" + 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")); - w.open(list(name + "_outputs_kw")); const auto outputs_name = "outputs"; - w << outputs_name; - w.close(); + w << list(*output_helper_name, outputs_name); w.open(list("list")); for (auto name : output_struct.get_field_names()) { w << list("cons", "\"" + name + "\"", output_struct.access_by_base_name(outputs_name, name)); @@ -318,10 +326,10 @@ struct SmtrModule { output_struct.write_definition(w); state_struct.write_definition(w); - if (input_kw_name) { - if (!output_kw_name) + if (input_helper_name) { + if (!output_helper_name) log_error("if keyword helpers are enabled, both input and output helper names are expected"); - write_keyword_helpers(w); + write_assoc_list_helpers(w); } write_eval(w); From 8ec9de00ec2b39e268cd5b8557a457cf0dca74af Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 20 May 2025 17:45:23 -0700 Subject: [PATCH 08/11] Use ir.inputs()/ir.outputs() --- backends/functional/smtlib_rosette.cc | 24 ++++-------------------- 1 file changed, 4 insertions(+), 20 deletions(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index ec116f1a2..f34cc7440 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -114,22 +114,6 @@ public: size_t i = field_names.at(name); return list(fields[i].accessor, std::move(record)); } - SExpr access_by_base_name(SExpr record, std::string base_name) - { - // Find the field by its base name - auto it = std::find_if(fields.begin(), fields.end(), [&](const Field &field) { return field.name == base_name; }); - if (it == fields.end()) { - log_error("Field with base name '%s' not found in struct '%s'.\n", base_name.c_str(), name.c_str()); - } - return list(it->accessor, std::move(record)); - } - std::vector get_field_names() - { - std::vector names; - for (auto field : fields) - names.push_back(field.name); - return names; - } }; std::string smt_const(RTLIL::Const const &c) { @@ -290,13 +274,13 @@ struct SmtrModule { w.open(list(*input_helper_name, inputs_name)); w.close(); w.open(list(input_struct.name)); - for (auto name : input_struct.get_field_names()) { + for (auto input : ir.inputs()) { w.push(); w.open(list("let")); w.push(); w.open(list()); w.open(list("assoc-result")); - w << list("assoc", "\"" + name + "\"", inputs_name); + w << list("assoc", "\"" + RTLIL::unescape_id(input->name) + "\"", inputs_name); w.pop(); w.open(list("if", "assoc-result")); w << list("cdr", "assoc-result"); @@ -312,8 +296,8 @@ struct SmtrModule { const auto outputs_name = "outputs"; w << list(*output_helper_name, outputs_name); w.open(list("list")); - for (auto name : output_struct.get_field_names()) { - w << list("cons", "\"" + name + "\"", output_struct.access_by_base_name(outputs_name, name)); + for (auto output : ir.outputs()) { + w << list("cons", "\"" + RTLIL::unescape_id(name) + "\"", output_struct.access("outputs", output->name)); } w.pop(); } From d8b27d41c03f9a5932c2364e519bc59d95067150 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Wed, 21 May 2025 21:31:07 -0700 Subject: [PATCH 09/11] Bugfix --- backends/functional/smtlib_rosette.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index f34cc7440..639efb46e 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -297,7 +297,7 @@ struct SmtrModule { w << list(*output_helper_name, outputs_name); w.open(list("list")); for (auto output : ir.outputs()) { - w << list("cons", "\"" + RTLIL::unescape_id(name) + "\"", output_struct.access("outputs", output->name)); + w << list("cons", "\"" + RTLIL::unescape_id(output->name) + "\"", output_struct.access("outputs", output->name)); } w.pop(); } From 9faa61dfc66a695565e48d634758aa11b1b58dee Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 26 May 2025 20:43:32 -0700 Subject: [PATCH 10/11] Remove gate on smt and rkt tests as per https://github.com/YosysHQ/yosys/pull/5128#issuecomment-2896280647 --- tests/functional/run-test.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/functional/run-test.sh b/tests/functional/run-test.sh index 9f70462ee..b9a0595f6 100755 --- a/tests/functional/run-test.sh +++ b/tests/functional/run-test.sh @@ -1,2 +1,2 @@ #!/usr/bin/env bash -pytest -v -m "not smt and not rkt" "$@" +pytest -v "$@" From 51560b0bf62c3f18317aa9513d189273cb48ee77 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 26 May 2025 21:46:53 -0700 Subject: [PATCH 11/11] Start adding Rosette simulation facilties --- tests/functional/simulate_rosette.py | 1 + tests/functional/simulate_rosette.rkt | 104 ++++++++++++++++++++++++++ 2 files changed, 105 insertions(+) create mode 100644 tests/functional/simulate_rosette.py create mode 100644 tests/functional/simulate_rosette.rkt diff --git a/tests/functional/simulate_rosette.py b/tests/functional/simulate_rosette.py new file mode 100644 index 000000000..9400a575a --- /dev/null +++ b/tests/functional/simulate_rosette.py @@ -0,0 +1 @@ +"""Python utilities for simulating Rosette code.""" \ No newline at end of file diff --git a/tests/functional/simulate_rosette.rkt b/tests/functional/simulate_rosette.rkt new file mode 100644 index 000000000..39038d0cd --- /dev/null +++ b/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. +; - : 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)))))