riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge https://github.com/cliffordwolf/yosys

This commit is contained in:
Andrew Zonenberg 2017-02-24 08:12:45 -08:00
parent 2eabe43efa a9c3acf5a2
commit 1f824fa643
7 changed files with 113 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Makefile
View File

@ -94,7 +94,7 @@ OBJS = kernel/version_$(GIT_REV).o
# is just a symlink to your actual ABC working directory, as 'make mrproper'
# will remove the 'abc' directory and you do not want to accidentally
# delete your work on ABC..
ABCREV = a2fcd1cc61a6
ABCREV = 8da4dc435b9f
ABCPULL = 1
ABCURL ?= https://bitbucket.org/alanmi/abc
ABCMKARGS = CC="$(CXX)" CXX="$(CXX)"
@ -478,7 +478,7 @@ ifeq ($(ENABLE_LIBYOSYS),1)
endif
uninstall:
$(INSTALL_SUDO) rm -vf $(addprefix $(DESTDIR)$(BINDIR),$(notdir $(TARGETS)))
$(INSTALL_SUDO) rm -vf $(addprefix $(DESTDIR)$(BINDIR)/,$(notdir $(TARGETS)))
$(INSTALL_SUDO) rm -rvf $(DESTDIR)$(DATDIR)
ifeq ($(ENABLE_LIBYOSYS),1)
$(INSTALL_SUDO) rm -vf $(DESTDIR)$(LIBDIR)/libyosys.so

67
backends/smt2/smt2.cc
View File

@ -32,8 +32,8 @@ struct Smt2Worker
CellTypes ct;
SigMap sigmap;
RTLIL::Module *module;
bool bvmode, memmode, wiresmode, verbose;
int idcounter;
bool bvmode, memmode, wiresmode, verbose, statebv;
int idcounter, statebv_width;
std::vector<std::string> decls, trans, hier;
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
@ -63,12 +63,41 @@ struct Smt2Worker
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 (width == 0) {
decl_str = stringf("(declare-fun |%s| (|%s_s|) Bool)\n", 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;
decls.push_back(decl_str + "\n");
}
Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose) :
ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode),
wiresmode(wiresmode), verbose(verbose), idcounter(0)
{
decls.push_back(stringf("(declare-sort |%s_s| 0)\n", get_id(module)));
decls.push_back(stringf("(declare-fun |%s_is| (|%s_s|) Bool)\n", get_id(module), get_id(module)));
statebv_width = 0;
statebv = bvmode && !memmode && false; // FIXME
makebits(stringf("%s_is", get_id(module)));
for (auto cell : module->cells())
for (auto &conn : cell->connections()) {
@ -162,8 +191,7 @@ struct Smt2Worker
if (fcache.count(bit) == 0) {
if (verbose) log("%*s-> external bool: %s\n", 2+2*GetSize(recursive_cells), "",
log_signal(bit));
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
get_id(module), idcounter, get_id(module), log_signal(bit)));
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(bit));
register_bool(bit, idcounter++);
}
@ -237,8 +265,7 @@ struct Smt2Worker
log_signal(sig.extract(i, j)));
for (auto bit : sig.extract(i, j))
log_assert(bit_driver.count(bit) == 0);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
get_id(module), idcounter, get_id(module), j, log_signal(sig.extract(i, j))));
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++);
}
@ -382,8 +409,7 @@ struct Smt2Worker
if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
get_id(module), idcounter, get_id(module), log_signal(cell->getPort("\\Q"))));
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort("\\Q")));
register_bool(cell->getPort("\\Q"), idcounter++);
recursive_cells.erase(cell);
return;
@ -410,8 +436,7 @@ struct Smt2Worker
if (cell->type.in("$ff", "$dff"))
{
registers.insert(cell);
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q")));
register_bv(cell->getPort("\\Q"), idcounter++);
recursive_cells.erase(cell);
return;
@ -422,8 +447,7 @@ struct Smt2Worker
registers.insert(cell);
decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))));
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
register_bv(cell->getPort("\\Y"), idcounter++);
recursive_cells.erase(cell);
return;
@ -559,24 +583,22 @@ struct Smt2Worker
if (w->port_output && !w->port_input) {
if (GetSize(w) > 1) {
if (bvmode) {
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
get_id(module), idcounter, get_id(module), GetSize(w), log_signal(sig)));
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(w), log_signal(sig));
register_bv(sig, idcounter++);
} else {
for (int i = 0; i < GetSize(w); i++) {
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
get_id(module), idcounter, get_id(module), log_signal(sig[i])));
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig[i]));
register_bool(sig[i], idcounter++);
}
}
} else {
decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n",
get_id(module), idcounter, get_id(module), log_signal(sig)));
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(sig));
register_bool(sig, idcounter++);
}
}
}
// FIXME (statebv)
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)));
@ -854,6 +876,11 @@ struct Smt2Worker
{
f << stringf("; yosys-smt2-module %s\n", get_id(module));
if (statebv)
f << stringf("(define-sort |%s_s| () (_ BitVec %d))\n", get_id(module), statebv_width);
else
f << stringf("(declare-sort |%s_s| 0)\n", get_id(module));
for (auto it : decls)
f << it;

25
backends/smt2/smtio.py
View File

@ -60,6 +60,7 @@ class SmtIo:
if opts is not None:
self.logic = opts.logic
self.solver = opts.solver
self.solver_opts = opts.solver_opts
self.debug_print = opts.debug_print
self.debug_file = opts.debug_file
self.dummy_file = opts.dummy_file
@ -71,6 +72,7 @@ class SmtIo:
else:
self.solver = "z3"
self.solver_opts = list()
self.debug_print = False
self.debug_file = None
self.dummy_file = None
@ -81,23 +83,26 @@ class SmtIo:
self.nocomments = False
if self.solver == "yices":
self.popen_vargs = ['yices-smt2', '--incremental']
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
if self.solver == "z3":
self.popen_vargs = ['z3', '-smt2', '-in']
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
if self.solver == "cvc4":
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2']
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + self.solver_opts
if self.solver == "mathsat":
self.popen_vargs = ['mathsat']
self.popen_vargs = ['mathsat'] + self.solver_opts
if self.solver == "boolector":
self.popen_vargs = ['boolector', '--smt2', '-i']
self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
self.unroll = True
if self.solver == "abc":
self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
if len(self.solver_opts) > 0:
self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]
else:
self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
self.logic_ax = False
self.unroll = True
self.noincr = True
@ -634,9 +639,10 @@ class SmtIo:
class SmtOpts:
def __init__(self):
self.shortopts = "s:v"
self.shortopts = "s:S:v"
self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.solver = "z3"
self.solver_opts = list()
self.debug_print = False
self.debug_file = None
self.dummy_file = None
@ -650,6 +656,8 @@ class SmtOpts:
def handle(self, o, a):
if o == "-s":
self.solver = a
elif o == "-S":
self.solver_opts.append(a)
elif o == "-v":
self.debug_print = True
elif o == "--unroll":
@ -678,6 +686,9 @@ class SmtOpts:
set SMT solver: z3, cvc4, yices, mathsat, boolector, dummy
default: z3
-S <opt>
pass <opt> as command line argument to the solver
--logic <smt2_logic>
use the specified SMT2 logic (e.g. QF_AUFBV)

10
frontends/ast/ast.cc
View File

@ -1104,7 +1104,10 @@ RTLIL::IdString AstModule::derive(RTLIL::Design *design, dict<RTLIL::IdString, R
rewrite_parameter:
para_info += stringf("%s=%s", child->str.c_str(), log_signal(RTLIL::SigSpec(parameters[para_id])));
delete child->children.at(0);
child->children[0] = AstNode::mkconst_bits(parameters[para_id].bits, (parameters[para_id].flags & RTLIL::CONST_FLAG_SIGNED) != 0);
if ((parameters[para_id].flags & RTLIL::CONST_FLAG_STRING) != 0)
child->children[0] = AstNode::mkconst_str(parameters[para_id].decode_string());
else
child->children[0] = AstNode::mkconst_bits(parameters[para_id].bits, (parameters[para_id].flags & RTLIL::CONST_FLAG_SIGNED) != 0);
parameters.erase(para_id);
continue;
}
@ -1118,7 +1121,10 @@ RTLIL::IdString AstModule::derive(RTLIL::Design *design, dict<RTLIL::IdString, R
for (auto param : parameters) {
AstNode *defparam = new AstNode(AST_DEFPARAM, new AstNode(AST_IDENTIFIER));
defparam->children[0]->str = param.first.str();
defparam->children.push_back(AstNode::mkconst_bits(param.second.bits, (param.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0));
if ((param.second.flags & RTLIL::CONST_FLAG_STRING) != 0)
defparam->children.push_back(AstNode::mkconst_str(param.second.decode_string()));
else
defparam->children.push_back(AstNode::mkconst_bits(param.second.bits, (param.second.flags & RTLIL::CONST_FLAG_SIGNED) != 0));
new_ast->children.push_back(defparam);
}

8
frontends/verilog/verilog_lexer.l
View File

@ -171,6 +171,10 @@ YOSYS_NAMESPACE_END
"while" { return TOK_WHILE; }
"repeat" { return TOK_REPEAT; }
"unique" { SV_KEYWORD(TOK_UNIQUE); }
"unique0" { SV_KEYWORD(TOK_UNIQUE); }
"priority" { SV_KEYWORD(TOK_PRIORITY); }
"always_comb" { SV_KEYWORD(TOK_ALWAYS); }
"always_ff" { SV_KEYWORD(TOK_ALWAYS); }
"always_latch" { SV_KEYWORD(TOK_ALWAYS); }
@ -366,7 +370,9 @@ import[ \t\r\n]+\"(DPI|DPI-C)\"[ \t\r\n]+function[ \t\r\n]+ {
"<<<" { return OP_SSHL; }
">>>" { return OP_SSHR; }
"::" { SV_KEYWORD(TOK_PACKAGESEP); }
"::" { return TOK_PACKAGESEP; }
"++" { return TOK_INCREMENT; }
"--" { return TOK_DECREMENT; }
"+:" { return TOK_POS_INDEXED; }
"-:" { return TOK_NEG_INDEXED; }

32
frontends/verilog/verilog_parser.y
View File

@ -117,12 +117,13 @@ static void free_attr(std::map<std::string, AstNode*> *al)
%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
%token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
%token TOK_RAND TOK_CONST TOK_CHECKER TOK_ENDCHECKER
%token TOK_INCREMENT TOK_DECREMENT TOK_UNIQUE TOK_PRIORITY
%type <ast> range range_or_multirange non_opt_range non_opt_multirange range_or_signed_int
%type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list
%type <string> opt_label tok_prim_wrapper hierarchical_id
%type <boolean> opt_signed
%type <al> attr
%type <boolean> opt_signed unique_case_attr
%type <al> attr case_attr
// operator precedence from low to high
%left OP_LOR
@ -1067,6 +1068,14 @@ simple_behavioral_stmt:
AstNode *node = new AstNode(AST_ASSIGN_EQ, $1, $4);
ast_stack.back()->children.push_back(node);
} |
lvalue TOK_INCREMENT {
AstNode *node = new AstNode(AST_ASSIGN_EQ, $1, new AstNode(AST_ADD, $1->clone(), AstNode::mkconst_int(1, true)));
ast_stack.back()->children.push_back(node);
} |
lvalue TOK_DECREMENT {
AstNode *node = new AstNode(AST_ASSIGN_EQ, $1, new AstNode(AST_SUB, $1->clone(), AstNode::mkconst_int(1, true)));
ast_stack.back()->children.push_back(node);
} |
lvalue OP_LE delay expr {
AstNode *node = new AstNode(AST_ASSIGN_LE, $1, $4);
ast_stack.back()->children.push_back(node);
@ -1158,7 +1167,7 @@ behavioral_stmt:
ast_stack.pop_back();
ast_stack.pop_back();
} |
attr case_type '(' expr ')' {
case_attr case_type '(' expr ')' {
AstNode *node = new AstNode(AST_CASE, $4);
ast_stack.back()->children.push_back(node);
ast_stack.push_back(node);
@ -1168,6 +1177,23 @@ behavioral_stmt:
ast_stack.pop_back();
};
unique_case_attr:
/* empty */ {
$$ = false;
} |
TOK_PRIORITY case_attr {
$$ = $2;
} |
TOK_UNIQUE case_attr {
$$ = true;
};
case_attr:
attr unique_case_attr {
if ($2) (*$1)["\\parallel_case"] = AstNode::mkconst_int(1, false);
$$ = $1;
};
case_type:
TOK_CASE {
case_type_stack.push_back(0);

4
kernel/calc.cc
View File

@ -291,7 +291,7 @@ static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Co
BigInteger pos = BigInteger(i) + offset;
if (pos < 0)
result.bits[i] = RTLIL::State::S0;
else if (pos >= arg1.bits.size())
else if (pos >= BigInteger(int(arg1.bits.size())))
result.bits[i] = sign_ext ? arg1.bits.back() : RTLIL::State::S0;
else
result.bits[i] = arg1.bits[pos.toInt()];
@ -342,7 +342,7 @@ static RTLIL::Const const_shift_shiftx(const RTLIL::Const &arg1, const RTLIL::Co
for (int i = 0; i < result_len; i++) {
BigInteger pos = BigInteger(i) + offset;
if (pos < 0 || pos >= arg1.bits.size())
if (pos < 0 || pos >= BigInteger(int(arg1.bits.size())))
result.bits[i] = other_bits;
else
result.bits[i] = arg1.bits[pos.toInt()];