Skip to content

Commit

Permalink
Valid SMT is emitted, improved test script
Browse files Browse the repository at this point in the history
  • Loading branch information
@RCoeurjoly
RCoeurjoly committed Jun 26, 2024
1 parent bb04a71 commit 8e3e5f5
Show file tree
Hide file tree
Showing 2 changed files with 86 additions and 40 deletions.
59 changes: 39 additions & 20 deletions backends/functional/smtlib.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -228,6 +228,7 @@ struct SmtPrintVisitor {
return format("#b%0", std::string(width, '0'));
}
};

struct SmtModule {
std::string name;
SmtScope scope;
Expand All @@ -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];
Expand All @@ -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];
Expand All @@ -268,35 +281,41 @@ struct SmtModule {

auto node_to_string = [&](FunctionalIR::Node n) { return scope[n.name()]; };
SmtPrintVisitor<decltype(node_to_string)> 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");
}
Expand Down
67 changes: 47 additions & 20 deletions tests/functional/single_cells/run-test.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 8e3e5f5

Please sign in to comment.