Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: azonenberg/yosys
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 088f9c9cab8d
Choose a base ref
...
head repository: azonenberg/yosys
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 106e44f40640
Choose a head ref
  • 4 commits
  • 4 files changed
  • 1 contributor

Commits on Mar 18, 2017

  1. Copy the full SHA
    1390e9a View commit details

Commits on Mar 19, 2017

  1. Copy the full SHA
    850f829 View commit details
  2. Copy the full SHA
    0ac72e7 View commit details

Commits on Mar 20, 2017

  1. Copy the full SHA
    106e44f View commit details
Showing with 208 additions and 43 deletions.
  1. +3 −6 backends/edif/edif.cc
  2. +121 −0 backends/edif/runtest.py
  3. +47 −9 backends/smt2/smt2.cc
  4. +37 −28 backends/smt2/smtio.py
9 changes: 3 additions & 6 deletions backends/edif/edif.cc
Original file line number Diff line number Diff line change
@@ -317,10 +317,7 @@ struct EdifBackend : public Backend {
*f << stringf(" (port (array %s %d) (direction %s))\n", EDIF_DEFR(wire->name, port_rename, b[0], b[1]), wire->width, dir);
for (int i = 0; i < wire->width; i++) {
RTLIL::SigSpec sig = sigmap(RTLIL::SigSpec(wire, i));
if (wire->upto)
net_join_db[sig].insert(stringf("(portRef (member %s %d))", EDIF_REF(wire->name), GetSize(wire)-i-1));
else
net_join_db[sig].insert(stringf("(portRef (member %s %d))", EDIF_REF(wire->name), i));
net_join_db[sig].insert(stringf("(portRef (member %s %d))", EDIF_REF(wire->name), GetSize(wire)-i-1));
}
}
}
@@ -363,11 +360,11 @@ struct EdifBackend : public Backend {
else if (sig.size() == 1)
net_join_db[sig[i]].insert(stringf("(portRef %s (instanceRef %s))", EDIF_REF(p.first), EDIF_REF(cell->name)));
else {
int member_idx = i;
int member_idx = GetSize(sig)-i-1;
auto m = design->module(cell->type);
if (m) {
auto w = m->wire(p.first);
if (w && w->upto)
if (w)
member_idx = GetSize(w)-i-1;
}
net_join_db[sig[i]].insert(stringf("(portRef (member %s %d) (instanceRef %s))",
121 changes: 121 additions & 0 deletions backends/edif/runtest.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,121 @@
#!/usr/bin/env python3

import os
import numpy as np

enable_upto = True
enable_offset = True
enable_hierarchy = True
enable_logic = True

def make_module(f, modname, width, subs):
print("module %s (A, B, C, X, Y, Z);" % modname, file=f)
inbits = list()
outbits = list()

for p in "ABC":
offset = np.random.randint(10) if enable_offset else 0
if enable_upto and np.random.randint(2):
print(" input [%d:%d] %s;" % (offset, offset+width-1, p), file=f)
else:
print(" input [%d:%d] %s;" % (offset+width-1, offset, p), file=f)
for i in range(offset, offset+width):
inbits.append("%s[%d]" % (p, i))

for p in "XYZ":
offset = np.random.randint(10) if enable_offset else 0
if enable_upto and np.random.randint(2):
print(" output [%d:%d] %s;" % (offset, offset+width-1, p), file=f)
else:
print(" output [%d:%d] %s;" % (offset+width-1, offset, p), file=f)
for i in range(offset, offset+width):
outbits.append("%s[%d]" % (p, i))

instidx = 0
subcandidates = list(subs.keys())

while len(outbits) > 0:
submod = None
if len(subcandidates):
submod = np.random.choice(subcandidates)
subcandidates.remove(submod)

if submod is None or 3*subs[submod] >= len(outbits):
for bit in outbits:
if enable_logic:
print(" assign %s = %s & ~%s;" % (bit, np.random.choice(inbits), np.random.choice(inbits)), file=f)
else:
print(" assign %s = %s;" % (bit, np.random.choice(inbits)), file=f)
break

instidx += 1
print(" %s inst%d (" % (submod, instidx), file=f)

for p in "ABC":
print(" .%s({%s})," % (p, ",".join(np.random.choice(inbits, subs[submod]))), file=f)

for p in "XYZ":
bits = list(np.random.choice(outbits, subs[submod], False))
for bit in bits:
outbits.remove(bit)
print(" .%s({%s})%s" % (p, ",".join(bits), "," if p != "Z" else ""), file=f)

print(" );", file=f);

print("endmodule", file=f)

with open("test_top.v", "w") as f:
if enable_hierarchy:
make_module(f, "sub1", 2, {})
make_module(f, "sub2", 3, {})
make_module(f, "sub3", 4, {})
make_module(f, "sub4", 8, {"sub1": 2, "sub2": 3, "sub3": 4})
make_module(f, "sub5", 8, {"sub1": 2, "sub2": 3, "sub3": 4})
make_module(f, "sub6", 8, {"sub1": 2, "sub2": 3, "sub3": 4})
make_module(f, "top", 32, {"sub4": 8, "sub5": 8, "sub6": 8})
else:
make_module(f, "top", 32, {})

os.system("set -x; ../../yosys -p 'synth_xilinx -top top; write_edif -pvector par test_syn.edif' test_top.v")

with open("test_syn.tcl", "w") as f:
print("read_edif test_syn.edif", file=f)
print("link_design", file=f)
print("write_verilog -force test_syn.v", file=f)

os.system("set -x; vivado -nojournal -nolog -mode batch -source test_syn.tcl")

with open("test_tb.v", "w") as f:
print("module tb;", file=f)
print(" reg [31:0] A, B, C;", file=f)
print(" wire [31:0] X, Y, Z;", file=f)
print("", file=f)
print(" top uut (", file=f)
print(" .A(A),", file=f)
print(" .B(B),", file=f)
print(" .C(C),", file=f)
print(" .X(X),", file=f)
print(" .Y(Y),", file=f)
print(" .Z(Z)", file=f)
print(" );", file=f)
print("", file=f)
print(" initial begin", file=f)
for i in range(100):
print(" A = 32'h%08x;" % np.random.randint(2**32), file=f)
print(" B = 32'h%08x;" % np.random.randint(2**32), file=f)
print(" C = 32'h%08x;" % np.random.randint(2**32), file=f)
print(" #10;", file=f)
print(" $display(\"%x %x %x\", X, Y, Z);", file=f)
print(" #10;", file=f)
print(" $finish;", file=f)
print(" end", file=f)
print("endmodule", file=f)

os.system("set -x; iverilog -o test_gold test_tb.v test_top.v")
os.system("set -x; iverilog -o test_gate test_tb.v test_syn.v ../../techlibs/xilinx/cells_sim.v")

os.system("set -x; ./test_gold > test_gold.out")
os.system("set -x; ./test_gate > test_gate.out")

os.system("set -x; md5sum test_gold.out test_gate.out")

56 changes: 47 additions & 9 deletions backends/smt2/smt2.cc
Original file line number Diff line number Diff line change
@@ -32,11 +32,11 @@ struct Smt2Worker
CellTypes ct;
SigMap sigmap;
RTLIL::Module *module;
bool bvmode, memmode, wiresmode, verbose, statebv;
bool bvmode, memmode, wiresmode, verbose, statebv, statedt;
dict<IdString, int> &mod_stbv_width;
int idcounter, statebv_width;

std::vector<std::string> decls, trans, hier;
std::vector<std::string> decls, trans, hier, dtmembers;
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
pool<Cell*> recursive_cells, registers;
@@ -78,6 +78,14 @@ struct Smt2Worker
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) {
@@ -89,12 +97,16 @@ struct Smt2Worker

if (!comment.empty())
decl_str += " ; " + comment;
decls.push_back(decl_str + "\n");

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, dict<IdString, int> &mod_stbv_width) :
Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, dict<IdString, int> &mod_stbv_width) :
ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
verbose(verbose), statebv(statebv), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
{
makebits(stringf("%s_is", get_id(module)));

@@ -583,8 +595,12 @@ struct Smt2Worker
}
else
{
decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
get_id(module), arrayid, get_id(module), abits, width, get_id(cell)));
if (statedt)
dtmembers.push_back(stringf(" (|%s#%d#0| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
get_id(module), arrayid, abits, width, get_id(cell)));
else
decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
get_id(module), arrayid, get_id(module), abits, width, get_id(cell)));

decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n",
get_id(module), get_id(cell), get_id(module), abits, width, get_id(module), arrayid));
@@ -649,6 +665,9 @@ struct Smt2Worker

if (statebv)
makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type));
if (statedt)
dtmembers.push_back(stringf(" (|%s_h %s| |%s_s|)\n",
get_id(module), get_id(cell->name), get_id(cell->type)));
else
decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n",
get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
@@ -1009,6 +1028,12 @@ struct Smt2Worker
if (statebv) {
f << stringf("(define-sort |%s_s| () (_ BitVec %d))\n", get_id(module), statebv_width);
mod_stbv_width[module->name] = statebv_width;
} else
if (statedt) {
f << stringf("(declare-datatype |%s_s| ((|%s_mk|\n", get_id(module), get_id(module));
for (auto it : dtmembers)
f << it;
f << stringf(")))\n");
} else
f << stringf("(declare-sort |%s_s| 0)\n", get_id(module));

@@ -1126,6 +1151,10 @@ struct Smt2Backend : public Backend {
log(" sort. As a side-effect this will prevent use of arrays to model\n");
log(" memories.\n");
log("\n");
log(" -stdt\n");
log(" Use SMT-LIB 2.6 style datatypes to represent a state instead of an\n");
log(" uninterpreted sort.\n");
log("\n");
log(" -nobv\n");
log(" disable support for BitVec (FixedSizeBitVectors theory). without this\n");
log(" option multi-bit wires are represented using the BitVec sort and\n");
@@ -1199,7 +1228,7 @@ struct Smt2Backend : public Backend {
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
std::ifstream template_f;
bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false;
bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;

log_header(design, "Executing SMT2 backend.\n");

@@ -1218,6 +1247,12 @@ struct Smt2Backend : public Backend {
}
if (args[argidx] == "-stbv") {
statebv = true;
statedt = false;
continue;
}
if (args[argidx] == "-stdt") {
statebv = false;
statedt = true;
continue;
}
if (args[argidx] == "-nobv") {
@@ -1264,6 +1299,9 @@ struct Smt2Backend : public Backend {
if (statebv)
*f << stringf("; yosys-smt2-stbv\n");

if (statedt)
*f << stringf("; yosys-smt2-stdt\n");

std::vector<RTLIL::Module*> sorted_modules;

// extract module dependencies
@@ -1304,7 +1342,7 @@ struct Smt2Backend : public Backend {

log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));

Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, mod_stbv_width);
Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width);
worker.run();
worker.write(*f);

65 changes: 37 additions & 28 deletions backends/smt2/smtio.py
Original file line number Diff line number Diff line change
@@ -53,6 +53,7 @@ def __init__(self, opts=None):
self.logic_ax = True
self.logic_uf = True
self.logic_bv = True
self.logic_dt = False
self.produce_models = True
self.smt2cache = [list()]
self.p = None
@@ -82,14 +83,42 @@ def __init__(self, opts=None):
self.info_stmts = list()
self.nocomments = False

if self.unroll:
self.logic_uf = False
self.unroll_idcnt = 0
self.unroll_buffer = ""
self.unroll_sorts = set()
self.unroll_objs = set()
self.unroll_decls = dict()
self.unroll_cache = dict()
self.unroll_stack = list()

self.start_time = time()

self.modinfo = dict()
self.curmod = None
self.topmod = None
self.setup_done = False

def setup(self):
assert not self.setup_done

if self.logic is None:
self.logic = ""
if self.logic_qf: self.logic += "QF_"
if self.logic_ax: self.logic += "A"
if self.logic_uf: self.logic += "UF"
if self.logic_bv: self.logic += "BV"
if self.logic_dt: self.logic = "ALL"

if self.solver == "yices":
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts

if self.solver == "z3":
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts

if self.solver == "cvc4":
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + self.solver_opts
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts

if self.solver == "mathsat":
self.popen_vargs = ['mathsat'] + self.solver_opts
@@ -116,33 +145,6 @@ def __init__(self, opts=None):
if not self.noincr:
self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)

if self.unroll:
self.logic_uf = False
self.unroll_idcnt = 0
self.unroll_buffer = ""
self.unroll_sorts = set()
self.unroll_objs = set()
self.unroll_decls = dict()
self.unroll_cache = dict()
self.unroll_stack = list()

self.start_time = time()

self.modinfo = dict()
self.curmod = None
self.topmod = None
self.setup_done = False

def setup(self):
assert not self.setup_done

if self.logic is None:
self.logic = ""
if self.logic_qf: self.logic += "QF_"
if self.logic_ax: self.logic += "A"
if self.logic_uf: self.logic += "UF"
if self.logic_bv: self.logic += "BV"

self.setup_done = True

if self.produce_models:
@@ -209,6 +211,9 @@ def unroll_stmt(self, stmt):
def write(self, stmt, unroll=True):
if stmt.startswith(";"):
self.info(stmt)
if not self.setup_done:
self.info_stmts.append(stmt)
return
elif not self.setup_done:
self.setup()

@@ -304,6 +309,10 @@ def info(self, stmt):
if self.logic is None:
self.logic_bv = False

if fields[1] == "yosys-smt2-stdt":
if self.logic is None:
self.logic_dt = True

if fields[1] == "yosys-smt2-module":
self.curmod = fields[2]
self.modinfo[self.curmod] = SmtModInfo()