From 8e3e5f5c5248e1480a87a5637d560d1f920977bb Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Wed, 26 Jun 2024 19:13:53 +0200 Subject: [PATCH] Valid SMT is emitted, improved test script --- backends/functional/smtlib.cc | 59 +++++++++++++------- tests/functional/single_cells/run-test.sh | 67 ++++++++++++++++------- 2 files changed, 86 insertions(+), 40 deletions(-) diff --git a/backends/functional/smtlib.cc b/backends/functional/smtlib.cc index 65541d8d8e9..671b3a76312 100644 --- a/backends/functional/smtlib.cc +++ b/backends/functional/smtlib.cc @@ -108,11 +108,11 @@ struct SmtPrintVisitor { } std::string zero_extend(Node, Node a, int, int out_width) { - return format("((_ zero_extend %1) %0)", np(a), out_width); + return format("((_ zero_extend %1) %0)", np(a), out_width - a.width()); } std::string sign_extend(Node, Node a, int, int out_width) { - return format("((_ sign_extend %1) %0)", np(a), out_width); + return format("((_ sign_extend %1) %0)", np(a), out_width - a.width()); } std::string concat(Node, Node a, int, Node b, int) { @@ -228,6 +228,7 @@ struct SmtPrintVisitor { return format("#b%0", std::string(width, '0')); } }; + struct SmtModule { std::string name; SmtScope scope; @@ -236,11 +237,24 @@ struct SmtModule { SmtModule(const std::string& module_name, FunctionalIR ir) : name(module_name), ir(std::move(ir)) {} + std::string replaceCharacters(const std::string& input) { + std::string result = input; + std::replace(result.begin(), result.end(), '$', '_'); // Replace $ with _ + + // Since \ is an escape character, we use a loop to replace it + size_t pos = 0; + while ((pos = result.find('\\', pos)) != std::string::npos) { + result.replace(pos, 1, "_"); + pos += 1; // Move past the replaced character + } + + return result; + } + void write(std::ostream& out) { SmtWriter writer(out); - + writer.print("(declare-fun %s () Bool)\n", name.c_str()); - writer.print("(declare-datatypes () ((Inputs (mk_inputs"); for (const auto& input : ir.inputs()) { std::string input_name = scope[input.first]; @@ -258,7 +272,6 @@ struct SmtModule { writer.print("(declare-fun state () (_ BitVec 1))\n"); writer.print("(define-fun %s_step ((state (_ BitVec 1)) (inputs Inputs)) Outputs\n", name.c_str()); - writer.print(" (let (\n"); for (const auto& input : ir.inputs()) { std::string input_name = scope[input.first]; @@ -268,35 +281,41 @@ struct SmtModule { auto node_to_string = [&](FunctionalIR::Node n) { return scope[n.name()]; }; SmtPrintVisitor visitor(node_to_string, scope); - writer.print(" (let (\n"); + + std::string nested_lets; for (auto it = ir.begin(); it != ir.end(); ++it) { const FunctionalIR::Node& node = *it; - if (ir.inputs().count(node.name()) > 0) { - continue; - } + if (ir.inputs().count(node.name()) > 0) continue; - std::string node_name = scope[node.name()]; + std::string node_name = replaceCharacters(scope[node.name()]); std::string node_expr = node.visit(visitor); - writer.print(" (%s %s)\n", node_name.c_str(), node_expr.c_str()); + + nested_lets += "(let (\n (" + node_name + " " + node_expr + "))\n"; } - writer.print(" )\n"); - writer.print(" (let (\n"); + nested_lets += " (let (\n"; for (const auto& output : ir.outputs()) { std::string output_name = scope[output.first]; - // writer.print(" (%s %s)\n", output_name.c_str(), scope[output_name].c_str()); + const std::string output_assignment = ir.get_output_node(output.first).name().c_str(); + nested_lets += " (" + output_name + " " + replaceCharacters(output_assignment).substr(1) + ")\n"; } - writer.print(" )\n"); + nested_lets += " )\n"; + nested_lets += " (mk_outputs\n"; - writer.print(" (mk_outputs\n"); for (const auto& output : ir.outputs()) { std::string output_name = scope[output.first]; - writer.print(" %s\n", output_name.c_str()); + nested_lets += " " + output_name + "\n"; } - writer.print(" )\n"); - writer.print(" )\n"); - writer.print(" )\n"); + nested_lets += " )\n"; + nested_lets += " )\n"; + + // Close the nested lets + for (size_t i = 0; i < ir.size() - ir.inputs().size(); ++i) { + nested_lets += " )\n"; + } + + writer.print("%s", nested_lets.c_str()); writer.print(" )\n"); writer.print(")\n"); } diff --git a/tests/functional/single_cells/run-test.sh b/tests/functional/single_cells/run-test.sh index fd1b178e45a..473c7faea51 100755 --- a/tests/functional/single_cells/run-test.sh +++ b/tests/functional/single_cells/run-test.sh @@ -54,29 +54,29 @@ run_smt_test() { # TODO: which SMT solver should be run? if z3 "${base_name}.smt2"; then echo "SMT file ${base_name}.smt2 is valid ." + smt_successful_files["$rtlil_file"]="Success" + # if python3 using_smtio.py "${base_name}.smt2"; then + # echo "Python script generated VCD file for $rtlil_file successfully." - if python3 using_smtio.py "${base_name}.smt2"; then - echo "Python script generated VCD file for $rtlil_file successfully." + # if [ -f "${base_name}.smt2.vcd" ]; then + # echo "VCD file ${base_name}.vcd generated successfully by Python." - if [ -f "${base_name}.smt2.vcd" ]; then - echo "VCD file ${base_name}.vcd generated successfully by Python." - - if ${BASE_PATH}yosys -p "read_rtlil $rtlil_file; sim -vcd ${base_name}_yosys.vcd -r ${base_name}.smt2.vcd -scope gold -timescale 1us"; then - echo "Yosys simulation for $rtlil_file completed successfully." - smt_successful_files["$rtlil_file"]="Success" - else - echo "Yosys simulation failed for $rtlil_file." - smt_failing_files["$rtlil_file"]="Yosys simulation failure" - fi - else + # if ${BASE_PATH}yosys -p "read_rtlil $rtlil_file; sim -vcd ${base_name}_yosys.vcd -r ${base_name}.smt2.vcd -scope gold -timescale 1us"; then + # echo "Yosys simulation for $rtlil_file completed successfully." + # smt_successful_files["$rtlil_file"]="Success" + # else + # echo "Yosys simulation failed for $rtlil_file." + # smt_failing_files["$rtlil_file"]="Yosys simulation failure" + # fi + # else - echo "Failed to generate VCD file (${base_name}.vcd) for $rtlil_file. " - smt_failing_files["$rtlil_file"]="VCD generation failure" - fi - else - echo "Failed to run Python script for $rtlil_file." - smt_failing_files["$rtlil_file"]="Python script failure" - fi + # echo "Failed to generate VCD file (${base_name}.vcd) for $rtlil_file. " + # smt_failing_files["$rtlil_file"]="VCD generation failure" + # fi + # else + # echo "Failed to run Python script for $rtlil_file." + # smt_failing_files["$rtlil_file"]="Python script failure" + # fi else echo "SMT file for $rtlil_file is invalid" smt_failing_files["$rtlil_file"]="Invalid SMT" @@ -135,6 +135,33 @@ run_all_tests() { return $return_code } +run_smt_tests() { + return_code=0 + for rtlil_file in rtlil/*.il; do + run_smt_test "$rtlil_file" + done + + echo "SMT tests results:" + if [ ${#smt_failing_files[@]} -eq 0 ]; then + echo "All files passed." + echo "The following files passed:" + for file in "${!smt_successful_files[@]}"; do + echo "$file" + done + else + echo "The following files failed:" + for file in "${!smt_failing_files[@]}"; do + echo "$file: ${smt_failing_files[$file]}" + done + echo "The following files passed:" + for file in "${!smt_successful_files[@]}"; do + echo "$file" + done + return_code=1 + fi + return $return_code +} + # If the script is being sourced, do not execute the tests if [[ "${BASH_SOURCE[0]}" == "${0}" ]]; then run_all_tests