aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/protobuf/.gitignore2
-rw-r--r--backends/protobuf/Makefile.inc10
-rw-r--r--backends/protobuf/protobuf.cc371
-rw-r--r--backends/smt2/smt2.cc13
-rw-r--r--backends/smt2/smtbmc.py45
-rw-r--r--backends/smt2/smtio.py11
6 files changed, 59 insertions, 393 deletions
diff --git a/backends/protobuf/.gitignore b/backends/protobuf/.gitignore
deleted file mode 100644
index 849b38d45..000000000
--- a/backends/protobuf/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-yosys.pb.cc
-yosys.pb.h
diff --git a/backends/protobuf/Makefile.inc b/backends/protobuf/Makefile.inc
deleted file mode 100644
index 9cac9dcaa..000000000
--- a/backends/protobuf/Makefile.inc
+++ /dev/null
@@ -1,10 +0,0 @@
-ifeq ($(ENABLE_PROTOBUF),1)
-
-backends/protobuf/yosys.pb.cc backends/protobuf/yosys.pb.h: misc/yosys.proto
- $(Q) cd misc && protoc --cpp_out "../backends/protobuf" yosys.proto
-
-backends/protobuf/protobuf.cc: backends/protobuf/yosys.pb.h
-
-OBJS += backends/protobuf/protobuf.o backends/protobuf/yosys.pb.o
-
-endif
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
deleted file mode 100644
index 384ce2e8e..000000000
--- a/backends/protobuf/protobuf.cc
+++ /dev/null
@@ -1,371 +0,0 @@
-/*
- * yosys -- Yosys Open SYnthesis Suite
- *
- * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
- * Copyright (C) 2018 Serge Bazanski <q3k@symbioticeda.com>
- *
- * 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 <google/protobuf/text_format.h>
-
-#include "kernel/rtlil.h"
-#include "kernel/register.h"
-#include "kernel/sigtools.h"
-#include "kernel/celltypes.h"
-#include "kernel/cellaigs.h"
-#include "kernel/log.h"
-#include "yosys.pb.h"
-
-USING_YOSYS_NAMESPACE
-PRIVATE_NAMESPACE_BEGIN
-
-struct ProtobufDesignSerializer
-{
- bool aig_mode_;
- bool use_selection_;
- yosys::pb::Design *pb_;
-
- Design *design_;
- Module *module_;
-
- SigMap sigmap_;
- int sigidcounter_;
- dict<SigBit, uint64_t> sigids_;
- pool<Aig> aig_models_;
-
-
- ProtobufDesignSerializer(bool use_selection, bool aig_mode) :
- aig_mode_(aig_mode), use_selection_(use_selection) { }
-
- string get_name(IdString name)
- {
- return RTLIL::unescape_id(name);
- }
-
-
- void serialize_parameters(google::protobuf::Map<std::string, yosys::pb::Parameter> *out,
- const dict<IdString, Const> &parameters)
- {
- for (auto &param : parameters) {
- std::string key = get_name(param.first);
-
-
- yosys::pb::Parameter pb_param;
-
- if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) {
- pb_param.set_str(param.second.decode_string());
- } else if (GetSize(param.second.bits) > 64) {
- pb_param.set_str(param.second.as_string());
- } else {
- pb_param.set_int_(param.second.as_int());
- }
-
- (*out)[key] = pb_param;
- }
- }
-
- void get_bits(yosys::pb::BitVector *out, SigSpec sig)
- {
- for (auto bit : sigmap_(sig)) {
- auto sig = out->add_signal();
-
- // Constant driver.
- if (bit.wire == nullptr) {
- if (bit == State::S0) sig->set_constant(sig->CONSTANT_DRIVER_LOW);
- else if (bit == State::S1) sig->set_constant(sig->CONSTANT_DRIVER_HIGH);
- else if (bit == State::Sz) sig->set_constant(sig->CONSTANT_DRIVER_Z);
- else sig->set_constant(sig->CONSTANT_DRIVER_X);
- continue;
- }
-
- // Signal - give it a unique identifier.
- if (sigids_.count(bit) == 0) {
- sigids_[bit] = sigidcounter_++;
- }
- sig->set_id(sigids_[bit]);
- }
- }
-
- void serialize_module(yosys::pb::Module* out, Module *module)
- {
- module_ = module;
- log_assert(module_->design == design_);
- sigmap_.set(module_);
- sigids_.clear();
- sigidcounter_ = 0;
-
- serialize_parameters(out->mutable_attribute(), module_->attributes);
-
- for (auto n : module_->ports) {
- Wire *w = module->wire(n);
- if (use_selection_ && !module_->selected(w))
- continue;
-
- yosys::pb::Module::Port pb_port;
- pb_port.set_direction(w->port_input ? w->port_output ?
- yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT : yosys::pb::DIRECTION_OUTPUT);
- get_bits(pb_port.mutable_bits(), w);
- (*out->mutable_port())[get_name(n)] = pb_port;
- }
-
- for (auto c : module_->cells()) {
- if (use_selection_ && !module_->selected(c))
- continue;
-
- yosys::pb::Module::Cell pb_cell;
- pb_cell.set_hide_name(c->name[0] == '$');
- pb_cell.set_type(get_name(c->type));
-
- if (aig_mode_) {
- Aig aig(c);
- if (aig.name.empty())
- continue;
- pb_cell.set_model(aig.name);
- aig_models_.insert(aig);
- }
- serialize_parameters(pb_cell.mutable_parameter(), c->parameters);
- serialize_parameters(pb_cell.mutable_attribute(), c->attributes);
-
- if (c->known()) {
- for (auto &conn : c->connections()) {
- yosys::pb::Direction direction = yosys::pb::DIRECTION_OUTPUT;
- if (c->input(conn.first))
- direction = c->output(conn.first) ? yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT;
- (*pb_cell.mutable_port_direction())[get_name(conn.first)] = direction;
- }
- }
- for (auto &conn : c->connections()) {
- yosys::pb::BitVector vec;
- get_bits(&vec, conn.second);
- (*pb_cell.mutable_connection())[get_name(conn.first)] = vec;
- }
-
- (*out->mutable_cell())[get_name(c->name)] = pb_cell;
- }
-
- for (auto w : module_->wires()) {
- if (use_selection_ && !module_->selected(w))
- continue;
-
- auto netname = out->add_netname();
- netname->set_hide_name(w->name[0] == '$');
- get_bits(netname->mutable_bits(), w);
- serialize_parameters(netname->mutable_attributes(), w->attributes);
- }
- }
-
-
- void serialize_models(google::protobuf::Map<string, yosys::pb::Model> *models)
- {
- for (auto &aig : aig_models_) {
- yosys::pb::Model pb_model;
- for (auto &node : aig.nodes) {
- auto pb_node = pb_model.add_node();
- if (node.portbit >= 0) {
- if (node.inverter) {
- pb_node->set_type(pb_node->TYPE_NPORT);
- } else {
- pb_node->set_type(pb_node->TYPE_PORT);
- }
- auto port = pb_node->mutable_port();
- port->set_portname(log_id(node.portname));
- port->set_bitindex(node.portbit);
- } else if (node.left_parent < 0 && node.right_parent < 0) {
- if (node.inverter) {
- pb_node->set_type(pb_node->TYPE_TRUE);
- } else {
- pb_node->set_type(pb_node->TYPE_FALSE);
- }
- } else {
- if (node.inverter) {
- pb_node->set_type(pb_node->TYPE_NAND);
- } else {
- pb_node->set_type(pb_node->TYPE_AND);
- }
- auto gate = pb_node->mutable_gate();
- gate->set_left(node.left_parent);
- gate->set_right(node.right_parent);
- }
- for (auto &op : node.outports) {
- auto pb_op = pb_node->add_out_port();
- pb_op->set_name(log_id(op.first));
- pb_op->set_bit_index(op.second);
- }
- }
- (*models)[aig.name] = pb_model;
- }
- }
-
- void serialize_design(yosys::pb::Design *pb, Design *design)
- {
- GOOGLE_PROTOBUF_VERIFY_VERSION;
- pb_ = pb;
- pb_->Clear();
- pb_->set_creator(yosys_version_str);
-
- design_ = design;
- design_->sort();
-
- auto modules = use_selection_ ? design_->selected_modules() : design_->modules();
- for (auto mod : modules) {
- yosys::pb::Module pb_mod;
- serialize_module(&pb_mod, mod);
- (*pb->mutable_modules())[mod->name.str()] = pb_mod;
- }
-
- serialize_models(pb_->mutable_models());
- }
-};
-
-struct ProtobufBackend : public Backend {
- ProtobufBackend(): Backend("protobuf", "write design to a Protocol Buffer file") { }
- void help() override
- {
- // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
- log("\n");
- log(" write_protobuf [options] [filename]\n");
- log("\n");
- log("Write a JSON netlist of the current design.\n");
- log("\n");
- log(" -aig\n");
- log(" include AIG models for the different gate types\n");
- log("\n");
- log(" -text\n");
- log(" output protobuf in Text/ASCII representation\n");
- log("\n");
- log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
- log("Yosys source code distribution.\n");
- log("\n");
- }
- void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
- {
- bool aig_mode = false;
- bool text_mode = false;
-
- size_t argidx;
- for (argidx = 1; argidx < args.size(); argidx++) {
- if (args[argidx] == "-aig") {
- aig_mode = true;
- continue;
- }
- if (args[argidx] == "-text") {
- text_mode = true;
- continue;
- }
- break;
- }
- extra_args(f, filename, args, argidx, !text_mode);
-
- log_header(design, "Executing Protobuf backend.\n");
-
- yosys::pb::Design pb;
- ProtobufDesignSerializer serializer(false, aig_mode);
- serializer.serialize_design(&pb, design);
-
- if (text_mode) {
- string out;
- google::protobuf::TextFormat::PrintToString(pb, &out);
- *f << out;
- } else {
- pb.SerializeToOstream(f);
- }
- }
-} ProtobufBackend;
-
-struct ProtobufPass : public Pass {
- ProtobufPass() : Pass("protobuf", "write design in Protobuf format") { }
- void help() override
- {
- // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
- log("\n");
- log(" protobuf [options] [selection]\n");
- log("\n");
- log("Write a JSON netlist of all selected objects.\n");
- log("\n");
- log(" -o <filename>\n");
- log(" write to the specified file.\n");
- log("\n");
- log(" -aig\n");
- log(" include AIG models for the different gate types\n");
- log("\n");
- log(" -text\n");
- log(" output protobuf in Text/ASCII representation\n");
- log("\n");
- log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
- log("Yosys source code distribution.\n");
- log("\n");
- }
- void execute(std::vector<std::string> args, RTLIL::Design *design) override
- {
- std::string filename;
- bool aig_mode = false;
- bool text_mode = false;
-
- size_t argidx;
- for (argidx = 1; argidx < args.size(); argidx++)
- {
- if (args[argidx] == "-o" && argidx+1 < args.size()) {
- filename = args[++argidx];
- continue;
- }
- if (args[argidx] == "-aig") {
- aig_mode = true;
- continue;
- }
- if (args[argidx] == "-text") {
- text_mode = true;
- continue;
- }
- break;
- }
- extra_args(args, argidx, design);
-
- std::ostream *f;
- std::stringstream buf;
-
- if (!filename.empty()) {
- rewrite_filename(filename);
- std::ofstream *ff = new std::ofstream;
- ff->open(filename.c_str(), text_mode ? std::ofstream::trunc : (std::ofstream::trunc | std::ofstream::binary));
- if (ff->fail()) {
- delete ff;
- log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
- }
- f = ff;
- } else {
- f = &buf;
- }
-
- yosys::pb::Design pb;
- ProtobufDesignSerializer serializer(true, aig_mode);
- serializer.serialize_design(&pb, design);
-
- if (text_mode) {
- string out;
- google::protobuf::TextFormat::PrintToString(pb, &out);
- *f << out;
- } else {
- pb.SerializeToOstream(f);
- }
-
- if (!filename.empty()) {
- delete f;
- } else {
- log("%s", buf.str().c_str());
- }
- }
-} ProtobufPass;
-
-PRIVATE_NAMESPACE_END;
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 54783cf1b..7434b13da 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -559,6 +559,9 @@ struct Smt2Worker
if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
{
registers.insert(cell);
+ SigBit q_bit = cell->getPort(ID::Q);
+ if (q_bit.is_wire())
+ decls.push_back(witness_signal("reg", 1, 0, "", idcounter, q_bit.wire));
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q)));
register_bool(cell->getPort(ID::Q), idcounter++);
recursive_cells.erase(cell);
@@ -589,9 +592,12 @@ struct Smt2Worker
if (cell->type.in(ID($ff), ID($dff)))
{
registers.insert(cell);
- for (auto chunk : cell->getPort(ID::Q).chunks())
+ int smtoffset = 0;
+ for (auto chunk : cell->getPort(ID::Q).chunks()) {
if (chunk.is_wire())
- decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire));
+ decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset));
+ smtoffset += chunk.width;
+ }
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
register_bv(cell->getPort(ID::Q), idcounter++);
recursive_cells.erase(cell);
@@ -1490,7 +1496,7 @@ struct Smt2Worker
return path;
}
- std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire)
+ std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire, int smtoffset = 0)
{
std::vector<std::string> hiername;
const char *wire_name = wire->name.c_str();
@@ -1508,6 +1514,7 @@ struct Smt2Worker
{ "offset", offset },
{ "width", width },
{ "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) },
+ { "smtoffset", smtoffset },
{ "path", witness_path(wire) },
}}).dump(line);
line += "\n";
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 5f05287de..cb21eb3aa 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -55,6 +55,7 @@ noinit = False
binarymode = False
keep_going = False
check_witness = False
+detect_loops = False
so = SmtOpts()
@@ -175,6 +176,10 @@ def usage():
check that the used witness file contains sufficient
constraints to force an assertion failure.
+ --detect-loops
+ check if states are unique in temporal induction counter examples
+ (this feature is experimental and incomplete)
+
""" + so.helpmsg())
sys.exit(1)
@@ -183,7 +188,7 @@ try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat",
"dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
- "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"])
+ "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"])
except:
usage()
@@ -264,6 +269,8 @@ for o, a in opts:
keep_going = True
elif o == "--check-witness":
check_witness = True
+ elif o == "--detect-loops":
+ detect_loops = True
elif so.handle(o, a):
pass
else:
@@ -446,7 +453,6 @@ assert topmod in smt.modinfo
if cexfile is not None:
if not got_topt:
- assume_skipped = 0
skip_steps = 0
num_steps = 0
@@ -492,7 +498,6 @@ if aimfile is not None:
latch_map = dict()
if not got_topt:
- assume_skipped = 0
skip_steps = 0
num_steps = 0
@@ -626,7 +631,6 @@ if aimfile is not None:
if inywfile is not None:
if not got_topt:
- assume_skipped = 0
skip_steps = 0
num_steps = 0
@@ -669,7 +673,7 @@ if inywfile is not None:
if common_end <= common_offset:
continue
- smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"])
+ smt_expr = smt.witness_net_expr(topmod, f"s{t}", wire)
if not smt_bool:
slice_high = common_end - offset - 1
@@ -969,6 +973,30 @@ def write_vcd_trace(steps_start, steps_stop, index):
vcd.set_time(steps_stop)
+def detect_state_loop(steps_start, steps_stop):
+ print_msg(f"Checking for loops in found induction counter example")
+ print_msg(f"This feature is experimental and incomplete")
+
+ path_list = sorted(smt.hiernets(topmod, regs_only=True))
+
+ mem_trace_data = collect_mem_trace_data(steps_start, steps_stop)
+
+ # Map state to index of step when it occurred
+ states = dict()
+
+ for i in range(steps_start, steps_stop):
+ value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
+ mem_state = sorted(
+ [(tuple(path), addr, data)
+ for path, addr, data in mem_trace_data.get(i, [])])
+ state = tuple(value_list), tuple(mem_state)
+ if state in states:
+ return (i, states[state])
+ else:
+ states[state] = i
+
+ return None
+
def char_ok_in_verilog(c,i):
if ('A' <= c <= 'Z'): return True
if ('a' <= c <= 'z'): return True
@@ -1267,7 +1295,8 @@ def write_yw_trace(steps_start, steps_stop, index, allregs=False):
sigs = seqs
for sig in sigs:
- step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"])))
+ value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig)))
+ step_values[sig["sig"]] = value
yw.step(step_values)
yw.end_trace()
@@ -1596,6 +1625,10 @@ if tempind:
print_anyconsts(num_steps)
print_failed_asserts(num_steps)
write_trace(step, num_steps+1, '%', allregs=True)
+ if detect_loops:
+ loop = detect_state_loop(step, num_steps+1)
+ if loop:
+ print_msg(f"Loop detected, increasing induction depth will not help. Step {loop[0]} = step {loop[1]}")
elif dumpall:
print_anyconsts(num_steps)
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 9af454cca..a73745896 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -701,7 +701,7 @@ class SmtIo:
if witness["type"] == "mem":
if allregs and not witness["rom"]:
width, size = witness["width"], witness["size"]
- witness = {**witness, "uninitialized": {"width": width * size, "offset": 0}}
+ witness = {**witness, "uninitialized": [{"width": width * size, "offset": 0}]}
if not witness["uninitialized"]:
continue
@@ -958,6 +958,15 @@ class SmtIo:
nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
return self.net_expr(nextmod, nextbase, path[1:])
+ def witness_net_expr(self, mod, base, witness):
+ net = self.net_expr(mod, base, witness["smtpath"])
+ is_bool = self.net_width(mod, witness["smtpath"]) == 1
+ if is_bool:
+ assert witness["width"] == 1
+ assert witness["smtoffset"] == 0
+ return net
+ return "((_ extract %d %d) %s)" % (witness["smtoffset"] + witness["width"] - 1, witness["smtoffset"], net)
+
def net_width(self, mod, net_path):
for i in range(len(net_path)-1):
assert mod in self.modinfo
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-23 18:38:00 +0000