From fd5918c811c701e82ba56d1040cd2acf327193f4 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Sat, 17 May 2025 14:10:23 -0700 Subject: [PATCH 01/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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))))) From 8a9d724873b74f6d0660407e1c47131f83717200 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 23 Jun 2025 19:20:06 -0700 Subject: [PATCH 12/16] Finish up functions and tests, TODO: CLI --- tests/functional/simulate_rosette.rkt | 211 ++++++++++++++++---------- 1 file changed, 132 insertions(+), 79 deletions(-) diff --git a/tests/functional/simulate_rosette.rkt b/tests/functional/simulate_rosette.rkt index 39038d0cd..aa838a5a0 100644 --- a/tests/functional/simulate_rosette.rkt +++ b/tests/functional/simulate_rosette.rkt @@ -1,104 +1,157 @@ ; Utilities for simulating Rosette programs. +; +; Tests can be run with `raco test `. #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: A list of association lists. The function will be called with each association list as +; inputs, and the state will be threaded through each call. +; +; Outputs: +; - A list of outputs, one for each cycle. The outputs are a list of the output objects generated by +; `function`. +(define (simulate-rosette #:function function #:initial-state initial-state #:inputs inputs) + + (define outputs-and-states + (drop (reverse (foldl (lambda (input acc) + (let* ([outputs (function input (cdr (car acc)))]) (cons outputs acc))) + (list (cons 'unused initial-state)) + inputs)) + 1)) + + (define outputs (map car outputs-and-states)) + + outputs) ; 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)) +; - inputs: association list mapping string name to bitwidth. +; - num-inputs: number of inputs to generate. +; TODO(@gussmith23): If `num-inputs` is more than the number of possible values, just enumerate. +(define (generate-inputs #:inputs inputs #:num-inputs num-inputs) + (define (generate-random-input inputs) + (map (lambda (pair) (cons (car pair) (bv (random (expt 2 (cdr pair))) (cdr pair)))) inputs)) + (for/list ([_ (range num-inputs)]) + (generate-random-input 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))])) +; Generates a clock signal for the given inputs. +; +; Given a string of inputs, one per clock cycle, this function generates a clock signal alongside the +; inputs. It does so by alternating the clock signal between 0 and 1 for each cycle, starting with 0. +; For example, if the inputs are (list inputs1 inputs2 inputs3), the output will be (list (cons (cons +; "clk" (bv 0 1)) inputs1) (cons (cons "clk" (bv 1 1)) inputs1) (cons (cons "clk" (bv 0 1)) inputs2) +; (cons (cons "clk" (bv 1 1)) inputs2) ... ). +; +; Inputs: +; - clock-name: The name of the clock signal. +; - inputs: A list of inputs in association list form, as output by `generate-inputs`. +; +; Outputs: +; - A list of association lists, each containing a new clock signal. Will be twice the length of the +; inputs list. +(define (generate-clock #:clock-name clock-name #:inputs inputs) + (apply append + (for/list ([this-cycle-inputs inputs]) + (list (cons (cons clock-name (bv 0 1)) this-cycle-inputs) + (cons (cons clock-name (bv 1 1)) this-cycle-inputs))))) ; This is what gets executed when the script is run. (module main racket/base - (require racket/cmdline)) + (require racket/cmdline) + + ; - 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. + ) (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))) + (require rackunit + (only-in rosette bv bvadd)) + (test-case "generate-inputs" + (check-equal? (length (generate-inputs #:inputs (list (cons "input1" 4)) #:num-inputs 10)) 10) + ; Check that this call generates a list of one-length lists, each containing a single association + ; list with the key "input1" and a random value. + (check-true (foldl (lambda (input acc) + (and acc (equal? (length input) 1) (equal? (car (first input)) "input1"))) + #t + (generate-inputs #:inputs (list (cons "input1" 4)) #:num-inputs 10)))) - ; Requesting fewer inputs than the number of possible values for the bitwidth. - (check-equal? (length (generate-inputs-for-one "input2" 3 5)) 5) + (test-case "generate-clock" + (define inputs + (list (list (cons "input1" (bv 4 4)) (cons "input2" (bv 3 3)) (cons "input3" (bv 2 2))) + (list (cons "input1" (bv 3 4)) (cons "input2" (bv 4 3)) (cons "input3" (bv 1 2))) + (list (cons "input1" (bv 2 4)) (cons "input2" (bv 5 3)) (cons "input3" (bv 0 2))))) - ; 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))) + (check-equal? (length (generate-clock #:clock-name "clk" #:inputs inputs)) 6) - ; 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))) + (check-equal? + (generate-clock #:clock-name "clk" #:inputs inputs) + (list (cons (cons "clk" (bv 0 1)) + (list (cons "input1" (bv 4 4)) (cons "input2" (bv 3 3)) (cons "input3" (bv 2 2)))) + (cons (cons "clk" (bv 1 1)) + (list (cons "input1" (bv 4 4)) (cons "input2" (bv 3 3)) (cons "input3" (bv 2 2)))) + (cons (cons "clk" (bv 0 1)) + (list (cons "input1" (bv 3 4)) (cons "input2" (bv 4 3)) (cons "input3" (bv 1 2)))) + (cons (cons "clk" (bv 1 1)) + (list (cons "input1" (bv 3 4)) (cons "input2" (bv 4 3)) (cons "input3" (bv 1 2)))) + (cons (cons "clk" (bv 0 1)) + (list (cons "input1" (bv 2 4)) (cons "input2" (bv 5 3)) (cons "input3" (bv 0 2)))) + (cons (cons "clk" (bv 1 1)) + (list (cons "input1" (bv 2 4)) (cons "input2" (bv 5 3)) (cons "input3" (bv 0 2))))))) + (test-case "simulate-rosette" - ; 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))))) + ; This function will take association lists as inputs, so the helper function is simply identity. + ; This is not generally true of Yosys-generated code. Similarly, this function uses an association + ; list for state, which is not what Yosys generates, but it's easier for testing. + ; + ; A one-stage adder. Inputs are registered in one clock cycle, and the output is the sum of the + ; two registered inputs. + (define (module-function inputs state) + (let* ([a (cdr (assoc "a" inputs))] + [b (cdr (assoc "b" inputs))] + [clk (cdr (assoc "clk" inputs))] + [old-clk (cdr (assoc "clk" state))] + [prev-a (cdr (assoc "prev-a" state))] + [prev-b (cdr (assoc "prev-b" state))] + [a-reg (cdr (assoc "a-reg" state))] + [b-reg (cdr (assoc "b-reg" state))] + [clk-ticked (and (equal? clk (bv 1 1)) (equal? old-clk (bv 0 1)))] + [new-a-reg (if clk-ticked prev-a a-reg)] + [new-b-reg (if clk-ticked prev-b b-reg)] + [out (list (cons "o" (bvadd new-a-reg new-b-reg)))] + [new-state (list (cons "prev-a" a) + (cons "a-reg" new-a-reg) + (cons "prev-b" b) + (cons "b-reg" new-b-reg) + (cons "clk" clk))]) + (cons out new-state))) + + (define outputs + (simulate-rosette #:function module-function + #:initial-state (list (cons "a-reg" (bv 0 4)) + (cons "b-reg" (bv 0 4)) + (cons "prev-a" (bv 0 4)) + (cons "prev-b" (bv 0 4)) + (cons "clk" (bv 0 1))) + #:inputs + (list (list (cons "clk" (bv 0 1)) (cons "a" (bv 4 4)) (cons "b" (bv 4 4))) + (list (cons "clk" (bv 1 1)) (cons "a" (bv 3 4)) (cons "b" (bv 0 4))) + (list (cons "clk" (bv 0 1)) (cons "a" (bv 10 4)) (cons "b" (bv 9 4))) + (list (cons "clk" (bv 1 1)) (cons "a" (bv 2 4)) (cons "b" (bv -1 4))) + (list (cons "clk" (bv 0 1)) (cons "a" (bv 4 4)) (cons "b" (bv -15 4))) + (list (cons "clk" (bv 1 1)) (cons "a" (bv 0 4)) (cons "b" (bv 0 4)))))) + + (check-equal? outputs + (list (list (cons "o" (bv 0 4))) + (list (cons "o" (bv 8 4))) + (list (cons "o" (bv 8 4))) + (list (cons "o" (bv 3 4))) + (list (cons "o" (bv 3 4))) + (list (cons "o" (bv -11 4))))))) From a1d68fe3bcddbf452832613822fce0235980b078 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Thu, 26 Jun 2025 17:44:12 -0700 Subject: [PATCH 13/16] Add option for using assoc list helpers in tests --- tests/functional/rkt_vcd.py | 113 +++++++++++++----- tests/functional/simulate_rosette.rkt | 157 -------------------------- tests/functional/test_functional.py | 8 +- 3 files changed, 91 insertions(+), 187 deletions(-) delete mode 100644 tests/functional/simulate_rosette.rkt diff --git a/tests/functional/rkt_vcd.py b/tests/functional/rkt_vcd.py index 1b2cf31e3..f06c2dc27 100644 --- a/tests/functional/rkt_vcd.py +++ b/tests/functional/rkt_vcd.py @@ -43,21 +43,37 @@ def write_vcd(filename: Path, signals: SignalStepMap, timescale='1 ns', date='to if change_time == time: f.write(f"{value} {signal_name}\n") -def simulate_rosette(rkt_file_path: Path, vcd_path: Path, num_steps: int, rnd: Random): + +def simulate_rosette( + rkt_file_path: Path, + vcd_path: Path, + num_steps: int, + rnd: Random, + use_assoc_list_helpers: bool = False, +): + """ + Args: + - use_assoc_list_helpers: If True, will use the association list helpers + in the Racket file. The file should have been generated with the + -assoc-list-helpers flag in the yosys command. + """ signals: dict[str, list[str]] = {} inputs: SignalWidthMap = {} outputs: SignalWidthMap = {} current_struct_name: str = "" - with open(rkt_file_path, 'r') as rkt_file: + with open(rkt_file_path, "r") as rkt_file: for line in rkt_file: - m = re.search(r'gold_(Inputs|Outputs|State)', line) + m = re.search(r"gold_(Inputs|Outputs|State)", line) if m: current_struct_name = m.group(1) - if current_struct_name == "State": break - elif not current_struct_name: continue # skip lines before structs - m = re.search(r'; (.+?)\b \(bitvector (\d+)\)', line) - if not m: continue # skip non matching lines (probably closing the struct) + if current_struct_name == "State": + break + elif not current_struct_name: + continue # skip lines before structs + m = re.search(r"; (.+?)\b \(bitvector (\d+)\)", line) + if not m: + continue # skip non matching lines (probably closing the struct) signal = m.group(1) width = int(m.group(2)) if current_struct_name == "Inputs": @@ -69,43 +85,86 @@ def simulate_rosette(rkt_file_path: Path, vcd_path: Path, num_steps: int, rnd: R step_list: list[int] = [] for step in range(num_steps): value = rnd.getrandbits(width) - binary_string = format(value, '0{}b'.format(width)) + binary_string = format(value, "0{}b".format(width)) step_list.append(binary_string) signals[signal] = step_list - test_rkt_file_path = rkt_file_path.with_suffix('.tst.rkt') - with open(test_rkt_file_path, 'w') as test_rkt_file: - test_rkt_file.writelines([ - '#lang rosette\n', - f'(require "{rkt_file_path.name}")\n', - ]) + test_rkt_file_path = rkt_file_path.with_suffix(".tst.rkt") + with open(test_rkt_file_path, "w") as test_rkt_file: + test_rkt_file.writelines( + [ + "#lang rosette\n", + f'(require "{rkt_file_path.name}")\n', + ] + ) for step in range(num_steps): this_step = f"step_{step}" value_list: list[str] = [] - for signal, width in inputs.items(): - value = signals[signal][step] - value_list.append(f"(bv #b{value} {width})") - gold_Inputs = f"(gold_Inputs {' '.join(value_list)})" + if use_assoc_list_helpers: + # Generate inputs as a list of cons pairs making up the + # association list. + for signal, width in inputs.items(): + value = signals[signal][step] + value_list.append(f'(cons "{signal}" (bv #b{value} {width}))') + else: + # Otherwise, we generate the inputs as a list of bitvectors. + for signal, width in inputs.items(): + value = signals[signal][step] + value_list.append(f"(bv #b{value} {width})") + gold_Inputs = ( + f"(gold_inputs_helper (list {' '.join(value_list)}))" + if use_assoc_list_helpers + else f"(gold_Inputs {' '.join(value_list)})" + ) gold_State = f"(cdr step_{step-1})" if step else "gold_initial" - test_rkt_file.write(f"(define {this_step} (gold {gold_Inputs} {gold_State})) (car {this_step})\n") + get_value_expr = ( + f"(gold_outputs_helper (car {this_step}))" + if use_assoc_list_helpers + else f"(car {this_step})" + ) + test_rkt_file.write( + f"(define {this_step} (gold {gold_Inputs} {gold_State})) {get_value_expr}\n" + ) + cmd = ["racket", test_rkt_file_path] - status = subprocess.run(cmd, capture_output=True) - assert status.returncode == 0, f"{cmd[0]} failed" + try: + status = subprocess.run(cmd, capture_output=True, check=True) + except subprocess.CalledProcessError as e: + raise RuntimeError( + f"Racket simulation failed with command: {cmd}\n" + f"Error: {e.stderr.decode()}" + ) from e for signal in outputs.keys(): signals[signal] = [] for line in status.stdout.decode().splitlines(): - m = re.match(r'\(gold_Outputs( \(bv \S+ \d+\))+\)', line) + m = ( + re.match(r"\(list( \(cons \"\S+\" \(bv \S+ \d+\)\))+\)", line) + if use_assoc_list_helpers + else re.match(r"\(gold_Outputs( \(bv \S+ \d+\))+\)", line) + ) assert m, f"Incomplete output definition {line!r}" - for output, (value, width) in zip(outputs.keys(), re.findall(r'\(bv (\S+) (\d+)\)', line)): + outputs_values_and_widths = ( + { + output: re.findall( + r"\(cons \"" + output + r"\" \(bv (\S+) (\d+)\)\)", line + )[0] + for output in outputs.keys() + }.items() + if use_assoc_list_helpers + else zip(outputs.keys(), re.findall(r"\(bv (\S+) (\d+)\)", line)) + ) + for output, (value, width) in outputs_values_and_widths: assert isinstance(value, str), f"Bad value {value!r}" - assert value.startswith(('#b', '#x')), f"Non-binary value {value!r}" - assert int(width) == outputs[output], f"Width mismatch for output {output!r} (got {width}, expected {outputs[output]})" - int_value = int(value[2:], 16 if value.startswith('#x') else 2) - binary_string = format(int_value, '0{}b'.format(width)) + assert value.startswith(("#b", "#x")), f"Non-binary value {value!r}" + assert ( + int(width) == outputs[output] + ), f"Width mismatch for output {output!r} (got {width}, expected {outputs[output]})" + int_value = int(value[2:], 16 if value.startswith("#x") else 2) + binary_string = format(int_value, "0{}b".format(width)) signals[output].append(binary_string) vcd_signals: SignalStepMap = {} diff --git a/tests/functional/simulate_rosette.rkt b/tests/functional/simulate_rosette.rkt deleted file mode 100644 index aa838a5a0..000000000 --- a/tests/functional/simulate_rosette.rkt +++ /dev/null @@ -1,157 +0,0 @@ -; Utilities for simulating Rosette programs. -; -; Tests can be run with `raco test `. -#lang racket/base - -(provide simulate-rosette) - -(require (only-in rosette bv) - 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. -; - initial-state: The initial state of the module, as generated by Yosys's `write_fuctional_rosette` -; backend. -; - inputs: A list of association lists. The function will be called with each association list as -; inputs, and the state will be threaded through each call. -; -; Outputs: -; - A list of outputs, one for each cycle. The outputs are a list of the output objects generated by -; `function`. -(define (simulate-rosette #:function function #:initial-state initial-state #:inputs inputs) - - (define outputs-and-states - (drop (reverse (foldl (lambda (input acc) - (let* ([outputs (function input (cdr (car acc)))]) (cons outputs acc))) - (list (cons 'unused initial-state)) - inputs)) - 1)) - - (define outputs (map car outputs-and-states)) - - outputs) - -; Inputs: -; - inputs: association list mapping string name to bitwidth. -; - num-inputs: number of inputs to generate. -; TODO(@gussmith23): If `num-inputs` is more than the number of possible values, just enumerate. -(define (generate-inputs #:inputs inputs #:num-inputs num-inputs) - (define (generate-random-input inputs) - (map (lambda (pair) (cons (car pair) (bv (random (expt 2 (cdr pair))) (cdr pair)))) inputs)) - (for/list ([_ (range num-inputs)]) - (generate-random-input inputs))) - -; Generates a clock signal for the given inputs. -; -; Given a string of inputs, one per clock cycle, this function generates a clock signal alongside the -; inputs. It does so by alternating the clock signal between 0 and 1 for each cycle, starting with 0. -; For example, if the inputs are (list inputs1 inputs2 inputs3), the output will be (list (cons (cons -; "clk" (bv 0 1)) inputs1) (cons (cons "clk" (bv 1 1)) inputs1) (cons (cons "clk" (bv 0 1)) inputs2) -; (cons (cons "clk" (bv 1 1)) inputs2) ... ). -; -; Inputs: -; - clock-name: The name of the clock signal. -; - inputs: A list of inputs in association list form, as output by `generate-inputs`. -; -; Outputs: -; - A list of association lists, each containing a new clock signal. Will be twice the length of the -; inputs list. -(define (generate-clock #:clock-name clock-name #:inputs inputs) - (apply append - (for/list ([this-cycle-inputs inputs]) - (list (cons (cons clock-name (bv 0 1)) this-cycle-inputs) - (cons (cons clock-name (bv 1 1)) this-cycle-inputs))))) - -; This is what gets executed when the script is run. -(module main racket/base - (require racket/cmdline) - - ; - 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. - ) - -(module+ test - (require rackunit - (only-in rosette bv bvadd)) - (test-case "generate-inputs" - (check-equal? (length (generate-inputs #:inputs (list (cons "input1" 4)) #:num-inputs 10)) 10) - ; Check that this call generates a list of one-length lists, each containing a single association - ; list with the key "input1" and a random value. - (check-true (foldl (lambda (input acc) - (and acc (equal? (length input) 1) (equal? (car (first input)) "input1"))) - #t - (generate-inputs #:inputs (list (cons "input1" 4)) #:num-inputs 10)))) - - (test-case "generate-clock" - (define inputs - (list (list (cons "input1" (bv 4 4)) (cons "input2" (bv 3 3)) (cons "input3" (bv 2 2))) - (list (cons "input1" (bv 3 4)) (cons "input2" (bv 4 3)) (cons "input3" (bv 1 2))) - (list (cons "input1" (bv 2 4)) (cons "input2" (bv 5 3)) (cons "input3" (bv 0 2))))) - - (check-equal? (length (generate-clock #:clock-name "clk" #:inputs inputs)) 6) - - (check-equal? - (generate-clock #:clock-name "clk" #:inputs inputs) - (list (cons (cons "clk" (bv 0 1)) - (list (cons "input1" (bv 4 4)) (cons "input2" (bv 3 3)) (cons "input3" (bv 2 2)))) - (cons (cons "clk" (bv 1 1)) - (list (cons "input1" (bv 4 4)) (cons "input2" (bv 3 3)) (cons "input3" (bv 2 2)))) - (cons (cons "clk" (bv 0 1)) - (list (cons "input1" (bv 3 4)) (cons "input2" (bv 4 3)) (cons "input3" (bv 1 2)))) - (cons (cons "clk" (bv 1 1)) - (list (cons "input1" (bv 3 4)) (cons "input2" (bv 4 3)) (cons "input3" (bv 1 2)))) - (cons (cons "clk" (bv 0 1)) - (list (cons "input1" (bv 2 4)) (cons "input2" (bv 5 3)) (cons "input3" (bv 0 2)))) - (cons (cons "clk" (bv 1 1)) - (list (cons "input1" (bv 2 4)) (cons "input2" (bv 5 3)) (cons "input3" (bv 0 2))))))) - (test-case "simulate-rosette" - - ; This function will take association lists as inputs, so the helper function is simply identity. - ; This is not generally true of Yosys-generated code. Similarly, this function uses an association - ; list for state, which is not what Yosys generates, but it's easier for testing. - ; - ; A one-stage adder. Inputs are registered in one clock cycle, and the output is the sum of the - ; two registered inputs. - (define (module-function inputs state) - (let* ([a (cdr (assoc "a" inputs))] - [b (cdr (assoc "b" inputs))] - [clk (cdr (assoc "clk" inputs))] - [old-clk (cdr (assoc "clk" state))] - [prev-a (cdr (assoc "prev-a" state))] - [prev-b (cdr (assoc "prev-b" state))] - [a-reg (cdr (assoc "a-reg" state))] - [b-reg (cdr (assoc "b-reg" state))] - [clk-ticked (and (equal? clk (bv 1 1)) (equal? old-clk (bv 0 1)))] - [new-a-reg (if clk-ticked prev-a a-reg)] - [new-b-reg (if clk-ticked prev-b b-reg)] - [out (list (cons "o" (bvadd new-a-reg new-b-reg)))] - [new-state (list (cons "prev-a" a) - (cons "a-reg" new-a-reg) - (cons "prev-b" b) - (cons "b-reg" new-b-reg) - (cons "clk" clk))]) - (cons out new-state))) - - (define outputs - (simulate-rosette #:function module-function - #:initial-state (list (cons "a-reg" (bv 0 4)) - (cons "b-reg" (bv 0 4)) - (cons "prev-a" (bv 0 4)) - (cons "prev-b" (bv 0 4)) - (cons "clk" (bv 0 1))) - #:inputs - (list (list (cons "clk" (bv 0 1)) (cons "a" (bv 4 4)) (cons "b" (bv 4 4))) - (list (cons "clk" (bv 1 1)) (cons "a" (bv 3 4)) (cons "b" (bv 0 4))) - (list (cons "clk" (bv 0 1)) (cons "a" (bv 10 4)) (cons "b" (bv 9 4))) - (list (cons "clk" (bv 1 1)) (cons "a" (bv 2 4)) (cons "b" (bv -1 4))) - (list (cons "clk" (bv 0 1)) (cons "a" (bv 4 4)) (cons "b" (bv -15 4))) - (list (cons "clk" (bv 1 1)) (cons "a" (bv 0 4)) (cons "b" (bv 0 4)))))) - - (check-equal? outputs - (list (list (cons "o" (bv 0 4))) - (list (cons "o" (bv 8 4))) - (list (cons "o" (bv 8 4))) - (list (cons "o" (bv 3 4))) - (list (cons "o" (bv 3 4))) - (list (cons "o" (bv -11 4))))))) diff --git a/tests/functional/test_functional.py b/tests/functional/test_functional.py index 7a09966d8..86eabef1e 100644 --- a/tests/functional/test_functional.py +++ b/tests/functional/test_functional.py @@ -74,7 +74,8 @@ def test_smt(cell, parameters, tmp_path, num_steps, rnd): yosys_sim(rtlil_file, vcd_functional_file, vcd_yosys_sim_file, getattr(cell, 'sim_preprocessing', '')) @pytest.mark.rkt -def test_rkt(cell, parameters, tmp_path, num_steps, rnd): +@pytest.mark.parametrize("use_assoc_list_helpers", [True, False]) +def test_rkt(cell, parameters, tmp_path, num_steps, rnd, use_assoc_list_helpers): import rkt_vcd rtlil_file = tmp_path / 'rtlil.il' @@ -83,8 +84,9 @@ def test_rkt(cell, parameters, tmp_path, num_steps, rnd): vcd_yosys_sim_file = tmp_path / 'yosys.vcd' cell.write_rtlil_file(rtlil_file, parameters) - yosys(f"read_rtlil {quote(rtlil_file)} ; clk2fflogic ; write_functional_rosette -provides {quote(rkt_file)}") - rkt_vcd.simulate_rosette(rkt_file, vcd_functional_file, num_steps, rnd(cell.name + "-rkt")) + use_assoc_helpers_flag = '-assoc-list-helpers' if use_assoc_list_helpers else '' + yosys(f"read_rtlil {quote(rtlil_file)} ; clk2fflogic ; write_functional_rosette -provides {use_assoc_helpers_flag} {quote(rkt_file)}") + rkt_vcd.simulate_rosette(rkt_file, vcd_functional_file, num_steps, rnd(cell.name + "-rkt"), use_assoc_list_helpers=use_assoc_list_helpers) yosys_sim(rtlil_file, vcd_functional_file, vcd_yosys_sim_file, getattr(cell, 'sim_preprocessing', '')) def test_print_graph(tmp_path): From 3c54d8aef791fbe000630ceb0e8af1c1f9f964ae Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 7 Jul 2025 10:38:32 +1200 Subject: [PATCH 14/16] tests/functional: Auto parallelize Use the unique cell name (cell type + parameters) for the vcd filename to avoid collisions when converting to fst. --- tests/functional/conftest.py | 2 +- tests/functional/rtlil_cells.py | 5 +++-- tests/functional/run-test.sh | 2 +- tests/functional/test_functional.py | 12 ++++++------ 4 files changed, 11 insertions(+), 10 deletions(-) diff --git a/tests/functional/conftest.py b/tests/functional/conftest.py index a9fbb3c59..fb00d4f22 100644 --- a/tests/functional/conftest.py +++ b/tests/functional/conftest.py @@ -31,4 +31,4 @@ def pytest_generate_tests(metafunc): seed1 = metafunc.config.getoption("seed") rnd = lambda seed2: random.Random('{}-{}'.format(seed1, seed2)) names, cases = generate_test_cases(per_cell, rnd) - metafunc.parametrize("cell,parameters", cases, ids=names) + metafunc.parametrize("name,cell,parameters", cases, ids=names) diff --git a/tests/functional/rtlil_cells.py b/tests/functional/rtlil_cells.py index 964d81ddf..ab7cd4e0c 100644 --- a/tests/functional/rtlil_cells.py +++ b/tests/functional/rtlil_cells.py @@ -374,8 +374,9 @@ def generate_test_cases(per_cell, rnd): for (name, parameters) in cell.generate_tests(rnd): if not name in seen_names: seen_names.add(name) - tests.append((cell, parameters)) - names.append(f'{cell.name}-{name}' if name != '' else cell.name) + full_name = f'{cell.name}-{name}' if name != '' else cell.name + tests.append((full_name, cell, parameters)) + names.append(full_name) if per_cell is not None and len(seen_names) >= per_cell: break return (names, tests) \ No newline at end of file diff --git a/tests/functional/run-test.sh b/tests/functional/run-test.sh index b9a0595f6..6786e93f1 100755 --- a/tests/functional/run-test.sh +++ b/tests/functional/run-test.sh @@ -1,2 +1,2 @@ #!/usr/bin/env bash -pytest -v "$@" +pytest -v -n auto "$@" diff --git a/tests/functional/test_functional.py b/tests/functional/test_functional.py index 86eabef1e..0553d6ecc 100644 --- a/tests/functional/test_functional.py +++ b/tests/functional/test_functional.py @@ -40,12 +40,12 @@ def yosys_sim(rtlil_file, vcd_reference_file, vcd_out_file, preprocessing = ""): capture_output=True, check=False) raise -def test_cxx(cell, parameters, tmp_path, num_steps, rnd): +def test_cxx(name, cell, parameters, tmp_path, num_steps, rnd): rtlil_file = tmp_path / 'rtlil.il' vcdharness_cc_file = base_path / 'tests/functional/vcd_harness.cc' cc_file = tmp_path / 'my_module_functional_cxx.cc' vcdharness_exe_file = tmp_path / 'a.out' - vcd_functional_file = tmp_path / 'functional.vcd' + vcd_functional_file = tmp_path / f'{name}.vcd' vcd_yosys_sim_file = tmp_path / 'yosys.vcd' cell.write_rtlil_file(rtlil_file, parameters) @@ -56,12 +56,12 @@ def test_cxx(cell, parameters, tmp_path, num_steps, rnd): yosys_sim(rtlil_file, vcd_functional_file, vcd_yosys_sim_file, getattr(cell, 'sim_preprocessing', '')) @pytest.mark.smt -def test_smt(cell, parameters, tmp_path, num_steps, rnd): +def test_smt(name, cell, parameters, tmp_path, num_steps, rnd): import smt_vcd rtlil_file = tmp_path / 'rtlil.il' smt_file = tmp_path / 'smtlib.smt' - vcd_functional_file = tmp_path / 'functional.vcd' + vcd_functional_file = tmp_path / f'{name}.vcd' vcd_yosys_sim_file = tmp_path / 'yosys.vcd' if hasattr(cell, 'smt_max_steps'): @@ -75,12 +75,12 @@ def test_smt(cell, parameters, tmp_path, num_steps, rnd): @pytest.mark.rkt @pytest.mark.parametrize("use_assoc_list_helpers", [True, False]) -def test_rkt(cell, parameters, tmp_path, num_steps, rnd, use_assoc_list_helpers): +def test_rkt(name, cell, parameters, tmp_path, num_steps, rnd, use_assoc_list_helpers): import rkt_vcd rtlil_file = tmp_path / 'rtlil.il' rkt_file = tmp_path / 'smtlib.rkt' - vcd_functional_file = tmp_path / 'functional.vcd' + vcd_functional_file = tmp_path / f'{name}.vcd' vcd_yosys_sim_file = tmp_path / 'yosys.vcd' cell.write_rtlil_file(rtlil_file, parameters) From 108a4ed4964cb3a70f34c44d232f23fb73897728 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 7 Jul 2025 10:45:51 +1200 Subject: [PATCH 15/16] tests/functional: Reduce CI to 100 steps Takes approx half the time, at least when testing locally. --- 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 6786e93f1..03e3b60f8 100755 --- a/tests/functional/run-test.sh +++ b/tests/functional/run-test.sh @@ -1,2 +1,2 @@ #!/usr/bin/env bash -pytest -v -n auto "$@" +pytest -v -n auto "$@" --steps 100 From dcf72ff8e2aa724b82ada89ad068b9308ed97a54 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 7 Jul 2025 11:27:37 +1200 Subject: [PATCH 16/16] Document tests/functional prereqs --- .../extending_yosys/test_suites.rst | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/docs/source/yosys_internals/extending_yosys/test_suites.rst b/docs/source/yosys_internals/extending_yosys/test_suites.rst index 3e5f45b94..6627fdbdd 100644 --- a/docs/source/yosys_internals/extending_yosys/test_suites.rst +++ b/docs/source/yosys_internals/extending_yosys/test_suites.rst @@ -14,6 +14,24 @@ compiler versions. For up to date information, including OS versions, refer to .. _Yosys Git repo: https://github.com/YosysHQ/yosys .. _the git actions page: https://github.com/YosysHQ/yosys/actions +Functional backend testing +-------------------------- + +Testing of the functional backend is controlled by the +``ENABLE_FUNCTIONAL_TESTS`` make variable. Setting it to a value of ``1``, +either when calling ``make test`` or in your ``Makefile.conf`` file, will enable +these additional tests. + +.. note:: + + The functional backend tests requires additional prerequisites to be + installed: + + - racket and z3, available via ``apt-get`` or similar. + - pytest and pytest-xdist, available via ``pip``; pytest-xdist-gnumake is + also recommended. + - rosette, available via ``raco`` (after installing racket). + .. todo:: are unit tests currently working ..