mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 03:32:29 +00:00
clang-format smtlib.cc
This commit is contained in:
Roland Coeurjoly
Emily Schmidt
parent
94ddbc9577
commit
4109fcedcf
1 changed files with 199 additions and 253 deletions
|
|
@ -17,8 +17,8 @@
|
|||
*
|
||||
*/
|
||||
|
||||
#include "kernel/yosys.h"
|
||||
#include "kernel/functionalir.h"
|
||||
#include "kernel/yosys.h"
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
|
@ -29,11 +29,10 @@ struct SmtScope {
|
|||
|
||||
SmtScope() {}
|
||||
|
||||
void reserve(const std::string& name) {
|
||||
used_names.insert(name);
|
||||
}
|
||||
void reserve(const std::string &name) { used_names.insert(name); }
|
||||
|
||||
std::string insert(IdString id) {
|
||||
std::string insert(IdString id)
|
||||
{
|
||||
std::string name = RTLIL::unescape_id(id);
|
||||
if (used_names.count(name) == 0) {
|
||||
used_names.insert(name);
|
||||
|
|
@ -50,7 +49,8 @@ struct SmtScope {
|
|||
}
|
||||
}
|
||||
|
||||
std::string operator[](IdString id) {
|
||||
std::string operator[](IdString id)
|
||||
{
|
||||
if (name_map.count(id)) {
|
||||
return name_map[id];
|
||||
} else {
|
||||
|
|
@ -64,7 +64,8 @@ struct SmtWriter {
|
|||
|
||||
SmtWriter(std::ostream &out) : stream(out) {}
|
||||
|
||||
void print(const char* fmt, ...) {
|
||||
void print(const char *fmt, ...)
|
||||
{
|
||||
va_list args;
|
||||
va_start(args, fmt);
|
||||
stream << vstringf(fmt, args);
|
||||
|
|
@ -72,24 +73,21 @@ struct SmtWriter {
|
|||
}
|
||||
};
|
||||
|
||||
template<class NodeNames>
|
||||
struct SmtPrintVisitor {
|
||||
template <class NodeNames> struct SmtPrintVisitor {
|
||||
using Node = FunctionalIR::Node;
|
||||
NodeNames np;
|
||||
SmtScope &scope;
|
||||
|
||||
SmtPrintVisitor(NodeNames np, SmtScope &scope)
|
||||
: np(np), scope(scope) {}
|
||||
SmtPrintVisitor(NodeNames np, SmtScope &scope) : np(np), scope(scope) {}
|
||||
|
||||
template<class T>
|
||||
std::string arg_to_string(T n) { return std::to_string(n); }
|
||||
template <class T> std::string arg_to_string(T n) { return std::to_string(n); }
|
||||
|
||||
std::string arg_to_string(std::string n) { return n; }
|
||||
|
||||
std::string arg_to_string(Node n) { return np(n); }
|
||||
|
||||
template<typename... Args>
|
||||
std::string format(std::string fmt, Args&&... args) {
|
||||
template <typename... Args> std::string format(std::string fmt, Args &&...args)
|
||||
{
|
||||
std::vector<std::string> arg_strings = {arg_to_string(std::forward<Args>(args))...};
|
||||
for (size_t i = 0; i < arg_strings.size(); ++i) {
|
||||
std::string placeholder = "%" + std::to_string(i);
|
||||
|
|
@ -103,133 +101,80 @@ struct SmtPrintVisitor {
|
|||
}
|
||||
std::string buf(Node, Node n) { return np(n); }
|
||||
|
||||
std::string slice(Node, Node a, int, int offset, int out_width) {
|
||||
std::string slice(Node, Node a, int, int offset, int out_width)
|
||||
{
|
||||
return format("(_ extract %1 %2 %0)", np(a), offset, offset + out_width - 1);
|
||||
}
|
||||
|
||||
std::string zero_extend(Node, Node a, int, int out_width) {
|
||||
return format("((_ zero_extend %1) %0)", np(a), out_width - a.width());
|
||||
}
|
||||
std::string zero_extend(Node, Node a, int, int 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 - a.width());
|
||||
}
|
||||
std::string sign_extend(Node, Node a, int, int out_width) { return format("((_ sign_extend %1) %0)", np(a), out_width - a.width()); }
|
||||
|
||||
std::string concat(Node, Node a, int, Node b, int) {
|
||||
return format("(concat %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string concat(Node, Node a, int, Node b, int) { return format("(concat %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string add(Node, Node a, Node b, int) {
|
||||
return format("(bvadd %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string add(Node, Node a, Node b, int) { return format("(bvadd %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string sub(Node, Node a, Node b, int) {
|
||||
return format("(bvsub %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string sub(Node, Node a, Node b, int) { return format("(bvsub %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string bitwise_and(Node, Node a, Node b, int) {
|
||||
return format("(bvand %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string bitwise_and(Node, Node a, Node b, int) { return format("(bvand %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string bitwise_or(Node, Node a, Node b, int) {
|
||||
return format("(bvor %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string bitwise_or(Node, Node a, Node b, int) { return format("(bvor %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string bitwise_xor(Node, Node a, Node b, int) {
|
||||
return format("(bvxor %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string bitwise_xor(Node, Node a, Node b, int) { return format("(bvxor %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string bitwise_not(Node, Node a, int) {
|
||||
return format("(bvnot %0)", np(a));
|
||||
}
|
||||
std::string bitwise_not(Node, Node a, int) { return format("(bvnot %0)", np(a)); }
|
||||
|
||||
std::string unary_minus(Node, Node a, int) {
|
||||
return format("(bvneg %0)", np(a));
|
||||
}
|
||||
std::string unary_minus(Node, Node a, int) { return format("(bvneg %0)", np(a)); }
|
||||
|
||||
std::string reduce_and(Node, Node a, int) {
|
||||
return format("(= %0 #b1)", np(a));
|
||||
}
|
||||
std::string reduce_and(Node, Node a, int) { return format("(= %0 #b1)", np(a)); }
|
||||
|
||||
std::string reduce_or(Node, Node a, int) {
|
||||
std::string reduce_or(Node, Node a, int)
|
||||
{
|
||||
std::stringstream ss;
|
||||
// We use ite to set the result to bit vector, to ensure appropriate type
|
||||
ss << "(ite (= " << np(a) << " #b" << std::string(a.width(), '0') << ") #b0 #b1)";
|
||||
return ss.str();
|
||||
}
|
||||
|
||||
std::string reduce_xor(Node, Node a, int) {
|
||||
return format("(bvxor_reduce %0)", np(a));
|
||||
}
|
||||
std::string reduce_xor(Node, Node a, int) { return format("(bvxor_reduce %0)", np(a)); }
|
||||
|
||||
std::string equal(Node, Node a, Node b, int) {
|
||||
return format("(= %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string equal(Node, Node a, Node b, int) { return format("(= %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string not_equal(Node, Node a, Node b, int) {
|
||||
return format("(distinct %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string not_equal(Node, Node a, Node b, int) { return format("(distinct %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string signed_greater_than(Node, Node a, Node b, int) {
|
||||
return format("(bvsgt %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string signed_greater_than(Node, Node a, Node b, int) { return format("(bvsgt %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string signed_greater_equal(Node, Node a, Node b, int) {
|
||||
return format("(bvsge %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string signed_greater_equal(Node, Node a, Node b, int) { return format("(bvsge %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string unsigned_greater_than(Node, Node a, Node b, int) {
|
||||
return format("(bvugt %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string unsigned_greater_than(Node, Node a, Node b, int) { return format("(bvugt %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string unsigned_greater_equal(Node, Node a, Node b, int) {
|
||||
return format("(bvuge %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string unsigned_greater_equal(Node, Node a, Node b, int) { return format("(bvuge %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string logical_shift_left(Node, Node a, Node b, int, int) {
|
||||
return format("(bvshl %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string logical_shift_left(Node, Node a, Node b, int, int) { return format("(bvshl %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string logical_shift_right(Node, Node a, Node b, int, int) {
|
||||
return format("(bvlshr %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string logical_shift_right(Node, Node a, Node b, int, int) { return format("(bvlshr %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string arithmetic_shift_right(Node, Node a, Node b, int, int) {
|
||||
return format("(bvashr %0 %1)", np(a), np(b));
|
||||
}
|
||||
std::string arithmetic_shift_right(Node, Node a, Node b, int, int) { return format("(bvashr %0 %1)", np(a), np(b)); }
|
||||
|
||||
std::string mux(Node, Node a, Node b, Node s, int) {
|
||||
return format("(ite %2 %0 %1)", np(a), np(b), np(s));
|
||||
}
|
||||
std::string mux(Node, Node a, Node b, Node s, int) { return format("(ite %2 %0 %1)", np(a), np(b), np(s)); }
|
||||
|
||||
std::string pmux(Node, Node a, Node b, Node s, int, int) {
|
||||
std::string pmux(Node, Node a, Node b, Node s, int, int)
|
||||
{
|
||||
// Assume s is a bit vector, combine a and b based on the selection bits
|
||||
return format("(pmux %0 %1 %2)", np(a), np(b), np(s));
|
||||
}
|
||||
|
||||
std::string constant(Node, RTLIL::Const value) {
|
||||
return format("#b%1", value.as_string());
|
||||
}
|
||||
std::string constant(Node, RTLIL::Const value) { return format("#b%1", value.as_string()); }
|
||||
|
||||
std::string input(Node, IdString name) {
|
||||
return format("%0", scope[name]);
|
||||
}
|
||||
std::string input(Node, IdString name) { return format("%0", scope[name]); }
|
||||
|
||||
std::string state(Node, IdString name) {
|
||||
return format("%0", scope[name]);
|
||||
}
|
||||
std::string state(Node, IdString name) { return format("%0", scope[name]); }
|
||||
|
||||
std::string memory_read(Node, Node mem, Node addr, int, int) {
|
||||
return format("(select %0 %1)", np(mem), np(addr));
|
||||
}
|
||||
std::string memory_read(Node, Node mem, Node addr, int, int) { return format("(select %0 %1)", np(mem), np(addr)); }
|
||||
|
||||
std::string memory_write(Node, Node mem, Node addr, Node data, int, int) {
|
||||
return format("(store %0 %1 %2)", np(mem), np(addr), np(data));
|
||||
}
|
||||
std::string memory_write(Node, Node mem, Node addr, Node data, int, int) { return format("(store %0 %1 %2)", np(mem), np(addr), np(data)); }
|
||||
|
||||
std::string undriven(Node, int width) {
|
||||
return format("#b%0", std::string(width, '0'));
|
||||
}
|
||||
std::string undriven(Node, int width) { return format("#b%0", std::string(width, '0')); }
|
||||
};
|
||||
|
||||
struct SmtModule {
|
||||
|
|
@ -237,10 +182,10 @@ struct SmtModule {
|
|||
SmtScope scope;
|
||||
FunctionalIR ir;
|
||||
|
||||
SmtModule(const std::string& module_name, FunctionalIR ir)
|
||||
: name(module_name), ir(std::move(ir)) {}
|
||||
SmtModule(const std::string &module_name, FunctionalIR ir) : name(module_name), ir(std::move(ir)) {}
|
||||
|
||||
std::string replaceCharacters(const std::string& input) {
|
||||
std::string replaceCharacters(const std::string &input)
|
||||
{
|
||||
std::string result = input;
|
||||
std::replace(result.begin(), result.end(), '$', '_'); // Replace $ with _
|
||||
|
||||
|
|
@ -254,7 +199,8 @@ struct SmtModule {
|
|||
return result;
|
||||
}
|
||||
|
||||
void write(std::ostream& out) {
|
||||
void write(std::ostream &out)
|
||||
{
|
||||
SmtWriter writer(out);
|
||||
|
||||
writer.print("(declare-fun %s () Bool)\n", name.c_str());
|
||||
|
|
@ -274,13 +220,13 @@ 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");
|
||||
writer.print("(define-fun %s_step ((state (_ BitVec 1)) (inputs Inputs)) Outputs", name.c_str());
|
||||
writer.print(" (let (");
|
||||
for (const auto &input : ir.inputs()) {
|
||||
std::string input_name = scope[input.first];
|
||||
writer.print(" (%s (%s inputs))\n", input_name.c_str(), input_name.c_str());
|
||||
writer.print(" (%s (%s inputs))", input_name.c_str(), input_name.c_str());
|
||||
}
|
||||
writer.print(" )\n");
|
||||
writer.print(" )");
|
||||
|
||||
auto node_to_string = [&](FunctionalIR::Node n) { return scope[n.name()]; };
|
||||
SmtPrintVisitor<decltype(node_to_string)> visitor(node_to_string, scope);
|
||||
|
|
@ -289,37 +235,38 @@ struct SmtModule {
|
|||
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 = replaceCharacters(scope[node.name()]);
|
||||
std::string node_expr = node.visit(visitor);
|
||||
|
||||
nested_lets += "(let (\n (" + node_name + " " + node_expr + "))\n";
|
||||
nested_lets += "(let ( (" + node_name + " " + node_expr + "))";
|
||||
}
|
||||
|
||||
nested_lets += " (let (\n";
|
||||
nested_lets += " (let (";
|
||||
for (const auto &output : ir.outputs()) {
|
||||
std::string output_name = scope[output.first];
|
||||
const std::string output_assignment = ir.get_output_node(output.first).name().c_str();
|
||||
nested_lets += " (" + output_name + " " + replaceCharacters(output_assignment).substr(1) + ")\n";
|
||||
nested_lets += " (" + output_name + " " + replaceCharacters(output_assignment).substr(1) + ")";
|
||||
}
|
||||
nested_lets += " )\n";
|
||||
nested_lets += " (mk_outputs\n";
|
||||
nested_lets += " )";
|
||||
nested_lets += " (mk_outputs";
|
||||
|
||||
for (const auto &output : ir.outputs()) {
|
||||
std::string output_name = scope[output.first];
|
||||
nested_lets += " " + output_name + "\n";
|
||||
nested_lets += " " + output_name;
|
||||
}
|
||||
nested_lets += " )\n";
|
||||
nested_lets += " )\n";
|
||||
nested_lets += " )";
|
||||
nested_lets += " )";
|
||||
|
||||
// Close the nested lets
|
||||
for (size_t i = 0; i < ir.size() - ir.inputs().size(); ++i) {
|
||||
nested_lets += " )\n";
|
||||
nested_lets += " )";
|
||||
}
|
||||
|
||||
writer.print("%s", nested_lets.c_str());
|
||||
writer.print(" )\n");
|
||||
writer.print(" )");
|
||||
writer.print(")\n");
|
||||
}
|
||||
};
|
||||
|
|
@ -327,11 +274,10 @@ struct SmtModule {
|
|||
struct FunctionalSmtBackend : public Backend {
|
||||
FunctionalSmtBackend() : Backend("functional_smt2", "Generate SMT-LIB from Functional IR") {}
|
||||
|
||||
void help() override {
|
||||
log("\nFunctional SMT Backend.\n\n");
|
||||
}
|
||||
void help() override { log("\nFunctional SMT Backend.\n\n"); }
|
||||
|
||||
void execute(std::ostream*& f, std::string filename, std::vector<std::string> args, RTLIL::Design* design) override {
|
||||
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
|
||||
{
|
||||
log_header(design, "Executing Functional SMT Backend.\n");
|
||||
|
||||
size_t argidx = 1;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue