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

7 files changed, 113 insertions, 37 deletions

diff --git a/Makefile b/Makefile
index 2773990a6..e779cf20d 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 932f5cd68..a4eff0850 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -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;
 
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index dda804efb..93cadd104 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -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)
 
diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 38a19a36f..06660102b 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -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);
 	}
 
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index ff2fa5753..091c1a029 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -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; }
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 1879ff441..9b2498694 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -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);
diff --git a/kernel/calc.cc b/kernel/calc.cc
index a24fa2abf..4a4840771 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -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()];