/* * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Clifford Wolf * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above * copyright notice and this permission notice appear in all copies. * * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. * */ #include "kernel/rtlil.h" #include "kernel/register.h" #include "kernel/sigtools.h" #include "kernel/celltypes.h" #include "kernel/log.h" #include USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN struct Smt2Worker { CellTypes ct; SigMap sigmap; RTLIL::Module *module; bool bvmode, memmode, wiresmode, verbose, statebv, statedt; dict &mod_stbv_width; int idcounter, statebv_width; std::vector decls, trans, hier, dtmembers; std::map bit_driver; std::set exported_cells, hiercells, hiercells_queue; pool recursive_cells, registers; std::map> fcache; std::map memarrays; std::map bvsizes; dict ids; const char *get_id(IdString n) { if (ids.count(n) == 0) { std::string str = log_id(n); for (int i = 0; i < GetSize(str); i++) { if (str[i] == '\\') str[i] = '/'; } ids[n] = strdup(str.c_str()); } return ids[n]; } template const char *get_id(T *obj) { return get_id(obj->name); } void makebits(std::string name, int width = 0, std::string comment = std::string()) { std::string decl_str; if (statebv) { if (width == 0) { decl_str = stringf("(define-fun |%s| ((state |%s_s|)) Bool (= ((_ extract %d %d) state) #b1))", name.c_str(), get_id(module), statebv_width, statebv_width); statebv_width += 1; } else { decl_str = stringf("(define-fun |%s| ((state |%s_s|)) (_ BitVec %d) ((_ extract %d %d) state))", name.c_str(), get_id(module), width, statebv_width+width-1, statebv_width); statebv_width += width; } } else if (statedt) { if (width == 0) { decl_str = stringf(" (|%s| Bool)", name.c_str()); } else { decl_str = stringf(" (|%s| (_ BitVec %d))", name.c_str(), width); } } else { if (width == 0) { decl_str = stringf("(declare-fun |%s| (|%s_s|) Bool)", name.c_str(), get_id(module)); } else { decl_str = stringf("(declare-fun |%s| (|%s_s|) (_ BitVec %d))", name.c_str(), get_id(module), width); } } if (!comment.empty()) decl_str += " ; " + comment; if (statedt) dtmembers.push_back(decl_str + "\n"); else decls.push_back(decl_str + "\n"); } Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, dict &mod_stbv_width) : ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode), verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0) { makebits(stringf("%s_is", get_id(module))); for (auto cell : module->cells()) for (auto &conn : cell->connections()) { bool is_input = ct.cell_input(cell->type, conn.first); bool is_output = ct.cell_output(cell->type, conn.first); if (is_output && !is_input) for (auto bit : sigmap(conn.second)) { if (bit_driver.count(bit)) log_error("Found multiple drivers for %s.\n", log_signal(bit)); bit_driver[bit] = cell; } else if (is_output || !is_input) log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n", log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type)); } } ~Smt2Worker() { for (auto &it : ids) free(it.second); ids.clear(); } const char *get_id(Module *m) { return get_id(m->name); } const char *get_id(Cell *c) { return get_id(c->name); } const char *get_id(Wire *w) { return get_id(w->name); } void register_bool(RTLIL::SigBit bit, int id) { if (verbose) log("%*s-> register_bool: %s %d\n", 2+2*GetSize(recursive_cells), "", log_signal(bit), id); sigmap.apply(bit); log_assert(fcache.count(bit) == 0); fcache[bit] = std::pair(id, -1); } void register_bv(RTLIL::SigSpec sig, int id) { if (verbose) log("%*s-> register_bv: %s %d\n", 2+2*GetSize(recursive_cells), "", log_signal(sig), id); log_assert(bvmode); sigmap.apply(sig); log_assert(bvsizes.count(id) == 0); bvsizes[id] = GetSize(sig); for (int i = 0; i < GetSize(sig); i++) { log_assert(fcache.count(sig[i]) == 0); fcache[sig[i]] = std::pair(id, i); } } void register_boolvec(RTLIL::SigSpec sig, int id) { if (verbose) log("%*s-> register_boolvec: %s %d\n", 2+2*GetSize(recursive_cells), "", log_signal(sig), id); log_assert(bvmode); sigmap.apply(sig); register_bool(sig[0], id); for (int i = 1; i < GetSize(sig); i++) sigmap.add(sig[i], RTLIL::State::S0); } std::string get_bool(RTLIL::SigBit bit, const char *state_name = "state") { sigmap.apply(bit); if (bit.wire == nullptr) return bit == RTLIL::State::S1 ? "true" : "false"; if (bit_driver.count(bit)) export_cell(bit_driver.at(bit)); sigmap.apply(bit); if (fcache.count(bit) == 0) { if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "", log_signal(bit)); makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(bit)); register_bool(bit, idcounter++); } auto f = fcache.at(bit); if (f.second >= 0) return stringf("(= ((_ extract %d %d) (|%s#%d| %s)) #b1)", f.second, f.second, get_id(module), f.first, state_name); return stringf("(|%s#%d| %s)", get_id(module), f.first, state_name); } std::string get_bool(RTLIL::SigSpec sig, const char *state_name = "state") { return get_bool(sig.as_bit(), state_name); } std::string get_bv(RTLIL::SigSpec sig, const char *state_name = "state") { log_assert(bvmode); sigmap.apply(sig); std::vector subexpr; SigSpec orig_sig; while (orig_sig != sig) { for (auto bit : sig) if (bit_driver.count(bit)) export_cell(bit_driver.at(bit)); orig_sig = sig; sigmap.apply(sig); } for (int i = 0, j = 1; i < GetSize(sig); i += j, j = 1) { if (sig[i].wire == nullptr) { while (i+j < GetSize(sig) && sig[i+j].wire == nullptr) j++; subexpr.push_back("#b"); for (int k = i+j-1; k >= i; k--) subexpr.back() += sig[k] == RTLIL::State::S1 ? "1" : "0"; continue; } if (fcache.count(sig[i]) && fcache.at(sig[i]).second == -1) { subexpr.push_back(stringf("(ite %s #b1 #b0)", get_bool(sig[i], state_name).c_str())); continue; } if (fcache.count(sig[i])) { auto t1 = fcache.at(sig[i]); while (i+j < GetSize(sig)) { if (fcache.count(sig[i+j]) == 0) break; auto t2 = fcache.at(sig[i+j]); if (t1.first != t2.first) break; if (t1.second+j != t2.second) break; j++; } if (t1.second == 0 && j == bvsizes.at(t1.first)) subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), t1.first, state_name)); else subexpr.push_back(stringf("((_ extract %d %d) (|%s#%d| %s))", t1.second + j - 1, t1.second, get_id(module), t1.first, state_name)); continue; } std::set seen_bits = { sig[i] }; while (i+j < GetSize(sig) && sig[i+j].wire && !fcache.count(sig[i+j]) && !seen_bits.count(sig[i+j])) seen_bits.insert(sig[i+j]), j++; if (verbose) log("%*s-> external bv: %s\n", 2+2*GetSize(recursive_cells), "", log_signal(sig.extract(i, j))); for (auto bit : sig.extract(i, j)) log_assert(bit_driver.count(bit) == 0); makebits(stringf("%s#%d", get_id(module), idcounter), j, log_signal(sig.extract(i, j))); subexpr.push_back(stringf("(|%s#%d| %s)", get_id(module), idcounter, state_name)); register_bv(sig.extract(i, j), idcounter++); } if (GetSize(subexpr) > 1) { std::string expr = "", end_str = ""; for (int i = GetSize(subexpr)-1; i >= 0; i--) { if (i > 0) expr += " (concat", end_str += ")"; expr += " " + subexpr[i]; } return expr.substr(1) + end_str; } else { log_assert(GetSize(subexpr) == 1); return subexpr[0]; } } void export_gate(RTLIL::Cell *cell, std::string expr) { RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").as_bit()); std::string processed_expr; for (char ch : expr) { if (ch == 'A') processed_expr += get_bool(cell->getPort("\\A")); else if (ch == 'B') processed_expr += get_bool(cell->getPort("\\B")); else if (ch == 'C') processed_expr += get_bool(cell->getPort("\\C")); else if (ch == 'D') processed_expr += get_bool(cell->getPort("\\D")); else if (ch == 'S') processed_expr += get_bool(cell->getPort("\\S")); else processed_expr += ch; } if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell)); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool %s) ; %s\n", get_id(module), idcounter, get_id(module), processed_expr.c_str(), log_signal(bit))); register_bool(bit, idcounter++); recursive_cells.erase(cell); } void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0) { RTLIL::SigSpec sig_a, sig_b; RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y")); bool is_signed = cell->getParam("\\A_SIGNED").as_bool(); int width = GetSize(sig_y); if (type == 's' || type == 'd' || type == 'b') { width = max(width, GetSize(cell->getPort("\\A"))); width = max(width, GetSize(cell->getPort("\\B"))); } if (cell->hasPort("\\A")) { sig_a = cell->getPort("\\A"); sig_a.extend_u0(width, is_signed); } if (cell->hasPort("\\B")) { sig_b = cell->getPort("\\B"); sig_b.extend_u0(width, is_signed && !
/*
 *  nextpnr -- Next Generation Place and Route
 *
 *  Copyright (C) 2018  gatecat <gatecat@ds0.me>
 *
 *  Permission to use, copy, modify, and/or distribute this software for any
 *  purpose with or without fee is hereby granted, provided that the above
 *  copyright notice and this permission notice appear in all copies.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *
 */

#ifndef UTIL_H
#define UTIL_H

#include <map>
#include <set>
#include <string>
#include "nextpnr.h"

#include "log.h"

NEXTPNR_NAMESPACE_BEGIN

// Get a value from a map-style container, returning default if value is not
// found
template <typename Container, typename KeyType, typename ValueType>
ValueType get_or_default(const Container &ct, const KeyType &key, ValueType def = ValueType())
{
    auto found = ct.find(key);
    if (found == ct.end())
        return def;
    else
        return found->second;
};

// Get a value from a map-style container, returning default if value is not
// found (forces string)
template <typename Container, typename KeyType>
std::string str_or_default(const Container &ct, const KeyType &key, std::string def = "")
{
    auto found = ct.find(key);
    if (found == ct.end())
        return def;
    else {
        return found->second;
    }
};

template <typename KeyType>
std::string str_or_default(const dict<KeyType, Property> &ct, const KeyType &key, std::string def = "")
{
    auto found = ct.find(key);
    if (found == ct.end())
        return def;
    else {
        if (!found->second.is_string)
            log_error("Expecting string value but got integer %d.\n", int(found->second.intval));
        return found->second.as_string();
    }
};

// Get a value from a map-style container, converting to int, and returning
// default if value is not found
template <typename Container, typename KeyType> int int_or_default(const Container &ct, const KeyType &key, int def = 0)
{
    auto found = ct.find(key);
    if (found == ct.end())
        return def;
    else
        return std::stoi(found->second);
};

template <typename KeyType> int int_or_default(const dict<KeyType, Property> &ct, const KeyType &key, int def = 0)
{
    auto found = ct.find(key);
    if (found == ct.end())
        return def;
    else {
        if (found->second.is_string) {
            try {
                return std::stoi(found->second.as_string());
            } catch (std::invalid_argument &e) {
                log_error("Expecting numeric value but got '%s'.\n", found->second.as_string().c_str());
            }
        } else
            return found->second.as_int64();
    }
};

// As above, but convert to bool
template <typename Container, typename KeyType>
bool bool_or_default(const Container &ct, const KeyType &key, bool def = false)
{
    return bool(int_or_default(ct, key, int(def)));
};

// Get only value from a forward iterator begin/end pair.
//
// Generates assertion failure if std::distance(begin, end) != 1.
template <typename ForwardIterator>
inline const typename ForwardIterator::reference get_only_value(ForwardIterator begin, ForwardIterator end)
{
    NPNR_ASSERT(begin != end);
    const typename ForwardIterator::reference ret = *begin;
    ++begin;
    NPNR_ASSERT(begin == end);
    return ret;
}

// Get only value from a forward iterator range pair.
//
// Generates assertion failure if std::distance(r.begin(), r.end()) != 1.
template <typename ForwardRange> inline auto get_only_value(ForwardRange r)
{
    auto b = r.begin();
    auto e = r.end();
    return get_only_value(b, e);
}

// From Yosys
// https://github.com/YosysHQ/yosys/blob/0fb4224ebca86156a1296b9210116d9a9cbebeed/kernel/utils.h#L131
template <typename T, typename C = std::less<T>> struct TopoSort
{
    bool analyze_loops, found_loops;
    std::map<T, std::set<T, C>, C> database;
    std::set<std::set<T, C>> loops;
    std::vector<T> sorted;

    TopoSort()
    {
        analyze_loops = true;
        found_loops = false;
    }

    void node(T n)
    {
        if (database.count(n) == 0)
            database[n] = std::set<T, C>();
    }

    void edge(T left, T right)
    {
        node(left);
        database[right].insert(left);
    }

    void sort_worker(const T &n, std::set<T, C> &marked_cells, std::set<T, C> &active_cells,
                     std::vector<T> &active_stack)
    {
        if (active_cells.count(n)) {
            found_loops = true;
            if (analyze_loops) {
                std::set<T, C> loop;
                for (int i = int(active_stack.size()) - 1; i >= 0; i--) {
                    loop.insert(active_stack[i]);
                    if (active_stack[i] == n)
                        break;
                }
                loops.insert(loop);
            }
            return;
        }

        if (marked_cells.count(n))
            return;

        if (!database.at(n).empty()) {
            if (analyze_loops)
                active_stack.push_back(n);
            active_cells.insert(n);

            for (auto &left_n : database.at(n))
                sort_worker(left_n, marked_cells, active_cells, active_stack);

            if (analyze_loops)
                active_stack.pop_back();
            active_cells.erase(n);
        }

        marked_cells.insert(n);
        sorted.push_back(n);
    }

    bool sort()
    {
        loops.clear();
        sorted.clear();
        found_loops = false;

        std::set<T, C> marked_cells;
        std::set<T, C> active_cells;
        std::vector<T> active_stack;

        for (auto &it : database)
            sort_worker(it.first, marked_cells, active_cells, active_stack);

        NPNR_ASSERT(sorted.size() == database.size());
        return !found_loops;
    }
};

template <typename T> struct reversed_range_t
{
    T &obj;
    explicit reversed_range_t(T &obj) : obj(obj){};
    auto begin() { return obj.rbegin(); }
    auto end() { return obj.rend(); }
};

template <typename T> reversed_range_t<T> reversed_range(T &obj) { return reversed_range_t<T>(obj); }

NEXTPNR_NAMESPACE_END

#endif
alue to a zero value.\n"); log("\n"); log(" module test(input clk, output reg [3:0] y);\n"); log(" always @(posedge clk)\n"); log(" y <= (y << 1) | ^y;\n"); log(" endmodule\n"); log("\n"); log("For this proof we create the following template (test.tpl).\n"); log("\n"); log(" ; we need QF_UFBV for this poof\n"); log(" (set-logic QF_UFBV)\n"); log("\n"); log(" ; insert the auto-generated code here\n"); log(" %%%%\n"); log("\n"); log(" ; declare two state variables s1 and s2\n"); log(" (declare-fun s1 () test_s)\n"); log(" (declare-fun s2 () test_s)\n"); log("\n"); log(" ; state s2 is the successor of state s1\n"); log(" (assert (test_t s1 s2))\n"); log("\n"); log(" ; we are looking for a model with y non-zero in s1\n"); log(" (assert (distinct (|test_n y| s1) #b0000))\n"); log("\n"); log(" ; we are looking for a model with y zero in s2\n"); log(" (assert (= (|test_n y| s2) #b0000))\n"); log("\n"); log(" ; is there such a model?\n"); log(" (check-sat)\n"); log("\n"); log("The following yosys script will create a 'test.smt2' file for our proof:\n"); log("\n"); log(" read_verilog test.v\n"); log(" hierarchy -check; proc; opt; check -assert\n"); log(" write_smt2 -bv -tpl test.tpl test.smt2\n"); log("\n"); log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n"); log("from non-zero to zero in the test design.\n"); log("\n"); } virtual void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) { std::ifstream template_f; bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false; log_header(design, "Executing SMT2 backend.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { if (args[argidx] == "-tpl" && argidx+1 < args.size()) { template_f.open(args[++argidx]); if (template_f.fail()) log_error("Can't open template file `%s'.\n", args[argidx].c_str()); continue; } if (args[argidx] == "-bv" || args[argidx] == "-mem") { log_warning("Options -bv and -mem are now the default. Support for -bv and -mem will be removed in the future.\n"); continue; } if (args[argidx] == "-stbv") { statebv = true; statedt = false; continue; } if (args[argidx] == "-stdt") { statebv = false; statedt = true; continue; } if (args[argidx] == "-nobv") { bvmode = false; memmode = false; continue; } if (args[argidx] == "-nomem") { memmode = false; continue; } if (args[argidx] == "-wires") { wiresmode = true; continue; } if (args[argidx] == "-verbose") { verbose = true; continue; } break; } extra_args(f, filename, args, argidx); if (template_f.is_open()) { std::string line; while (std::getline(template_f, line)) { int indent = 0; while (indent < GetSize(line) && (line[indent] == ' ' || line[indent] == '\t')) indent++; if (line.substr(indent, 2) == "%%") break; *f << line << std::endl; } } *f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str); if (!bvmode) *f << stringf("; yosys-smt2-nobv\n"); if (!memmode) *f << stringf("; yosys-smt2-nomem\n"); if (statebv) *f << stringf("; yosys-smt2-stbv\n"); if (statedt) *f << stringf("; yosys-smt2-stdt\n"); std::vector sorted_modules; // extract module dependencies std::map> module_deps; for (auto &mod_it : design->modules_) { module_deps[mod_it.second] = std::set(); for (auto &cell_it : mod_it.second->cells_) if (design->modules_.count(cell_it.second->type) > 0) module_deps[mod_it.second].insert(design->modules_.at(cell_it.second->type)); } // simple good-enough topological sort // (O(n*m) on n elements and depth m) while (module_deps.size() > 0) { size_t sorted_modules_idx = sorted_modules.size(); for (auto &it : module_deps) { for (auto &dep : it.second) if (module_deps.count(dep) > 0) goto not_ready_yet; // log("Next in topological sort: %s\n", RTLIL::id2cstr(it.first->name)); sorted_modules.push_back(it.first); not_ready_yet:; } if (sorted_modules_idx == sorted_modules.size()) log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", RTLIL::id2cstr(module_deps.begin()->first->name)); while (sorted_modules_idx < sorted_modules.size()) module_deps.erase(sorted_modules.at(sorted_modules_idx++)); } dict mod_stbv_width; Module *topmod = design->top_module(); std::string topmod_id; for (auto module : sorted_modules) { if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn()) continue; log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width); worker.run(); worker.write(*f); if (module == topmod) topmod_id = worker.get_id(module); } if (topmod) *f << stringf("; yosys-smt2-topmod %s\n", topmod_id.c_str()); *f << stringf("; end of yosys output\n"); if (template_f.is_open()) { std::string line; while (std::getline(template_f, line)) *f << line << std::endl; } } } Smt2Backend; PRIVATE_NAMESPACE_END