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

Makefile

@@ -86,7 +86,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 = f8cadfe3861f
+ABCREV = a2fcd1cc61a6
 ABCPULL = 1
 ABCURL ?= https://bitbucket.org/alanmi/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)"

README.md

@@ -46,7 +46,7 @@ Getting Started
 
 You need a C++ compiler with C++11 support (up-to-date CLANG or GCC is
 recommended) and some standard tools such as GNU Flex, GNU Bison, and GNU Make.
-TCL, readline and libffi are optional (see ENABLE_* settings in Makefile).
+TCL, readline and libffi are optional (see ``ENABLE_*`` settings in Makefile).
 Xdot (graphviz) is used by the ``show`` command in yosys to display schematics.
 For example on Ubuntu Linux 16.04 LTS the following commands will install all
 prerequisites for building yosys:
@@ -372,16 +372,17 @@ Verilog Attributes and non-standard features
 Non-standard or SystemVerilog features for formal verification
 ==============================================================
 
-- Support for ``assert``, ``assume``, and ``restrict`` is enabled when
+- Support for ``assert``, ``assume``, ``restrict``, and ``cover'' is enabled
-  ``read_verilog`` is called with ``-formal``.
+  when ``read_verilog`` is called with ``-formal``.
 
 - The system task ``$initstate`` evaluates to 1 in the initial state and
   to 0 otherwise.
 
-- The system task ``$anyconst`` evaluates to any constant value.
+- The system task ``$anyconst`` evaluates to any constant value. This is
+  equivalent to declaring a reg as ``const rand``.
 
 - The system task ``$anyseq`` evaluates to any value, possibly a different
-  value in each cycle.
+  value in each cycle. This is equivalent to declaring a reg as ``rand``.
 
 - The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are
   supported in any clocked block.
@@ -400,12 +401,14 @@ from SystemVerilog:
   form. In module context: ``assert property (<expression>);`` and within an
   always block: ``assert(<expression>);``. It is transformed to a $assert cell.
 
-- The ``assume`` and ``restrict`` statements from SystemVerilog are also
+- The ``assume``, ``restrict``, and ``cover`` statements from SystemVerilog are
-  supported. The same limitations as with the ``assert`` statement apply.
+  also supported. The same limitations as with the ``assert`` statement apply.
 
 - The keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic``
   and ``bit`` are supported.
 
+- Declaring free variables with ``rand`` and ``const rand`` is supported.
+
 - SystemVerilog packages are supported. Once a SystemVerilog file is read
   into a design with ``read_verilog``, all its packages are available to
   SystemVerilog files being read into the same design afterwards.

backends/smt2/smt2.cc

@@ -662,19 +662,25 @@ struct Smt2Worker
 
 		if (verbose) log("=> export logic driving asserts\n");
 
-		vector<string> assert_list, assume_list;
+		vector<string> assert_list, assume_list, cover_list;
 		for (auto cell : module->cells())
-			if (cell->type.in("$assert", "$assume")) {
+			if (cell->type.in("$assert", "$assume", "$cover")) {
 				string name_a = get_bool(cell->getPort("\\A"));
 				string name_en = get_bool(cell->getPort("\\EN"));
 				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("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
+				if (cell->type == "$cover")
-						get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
+					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
+							get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
+				else
+					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
+							get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
 				if (cell->type == "$assert")
 					assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
-				else
+				else if (cell->type == "$assume")
 					assume_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
+				else if (cell->type == "$cover")
+					cover_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
 			}
 
 		for (int iter = 1; !registers.empty(); iter++)

backends/smt2/smtbmc.py

@@ -29,11 +29,14 @@ num_steps = 20
 append_steps = 0
 vcdfile = None
 cexfile = None
-aigprefix = None
+aimfile = None
+aiwfile = None
+aigheader = True
 vlogtbfile = None
 inconstr = list()
 outconstr = None
 gentrace = False
+covermode = False
 tempind = False
 dumpall = False
 assume_skipped = None
@@ -59,6 +62,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
     -i
         instead of BMC run temporal induction
 
+    -c
+        instead of regular BMC run cover analysis
+
     -m <module_name>
         name of the top module
 
@@ -73,6 +79,14 @@ yosys-smtbmc [options] <yosys_smt2_output>
         and AIGER witness file. The file names are <prefix>.aim for
         the map file and <prefix>.aiw for the witness file.
 
+    --aig <aim_filename>:<aiw_filename>
+        like above, but for map files and witness files that do not
+        share a filename prefix (or use differen file extensions).
+
+    --aig-noheader
+        the AIGER witness file does not include the status and
+        properties lines.
+
     --noinfo
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
@@ -110,8 +124,8 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
 
 try:
-    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
+    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=",
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader",
              "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="])
 except:
     usage()
@@ -140,7 +154,13 @@ for o, a in opts:
     elif o == "--cex":
         cexfile = a
     elif o == "--aig":
-        aigprefix = a
+        if ":" in a:
+            aimfile, aiwfile = a.split(":")
+        else:
+            aimfile = a + ".aim"
+            aiwfile = a + ".aiw"
+    elif o == "--aig-noheader":
+        aigheader = False
     elif o == "--dump-vcd":
         vcdfile = a
     elif o == "--dump-vlogtb":
@@ -157,6 +177,8 @@ for o, a in opts:
         tempind = True
     elif o == "-g":
         gentrace = True
+    elif o == "-c":
+        covermode = True
     elif o == "-m":
         topmod = a
     elif so.handle(o, a):
@@ -167,6 +189,8 @@ for o, a in opts:
 if len(args) != 1:
     usage()
 
+if sum([tempind, gentrace, covermode]) > 1:
+    usage()
 
 constr_final_start = None
 constr_asserts = defaultdict(list)
@@ -375,7 +399,7 @@ if cexfile is not None:
                 skip_steps = max(skip_steps, step)
                 num_steps = max(num_steps, step+1)
 
-if aigprefix is not None:
+if aimfile is not None:
     input_map = dict()
     init_map = dict()
     latch_map = dict()
@@ -385,7 +409,7 @@ if aigprefix is not None:
         skip_steps = 0
         num_steps = 0
 
-    with open(aigprefix + ".aim", "r") as f:
+    with open(aimfile, "r") as f:
         for entry in f.read().splitlines():
             entry = entry.split()
 
@@ -406,11 +430,14 @@ if aigprefix is not None:
 
             assert False
 
-    with open(aigprefix + ".aiw", "r") as f:
+    with open(aiwfile, "r") as f:
         got_state = False
         got_ffinit = False
         step = 0
 
+        if not aigheader:
+            got_state = True
+
         for entry in f.read().splitlines():
             if len(entry) == 0 or entry[0] in "bcjfu.":
                 continue
@@ -458,13 +485,30 @@ if aigprefix is not None:
                     bitidx = init_map[i][1]
 
                     path = smt.get_path(topmod, name)
-                    width = smt.net_width(topmod, path)
+
+                    if not smt.net_exists(topmod, path):
+                        match = re.match(r"(.*)\[(\d+)\]$", path[-1])
+                        if match:
+                            path[-1] = match.group(1)
+                            addr = int(match.group(2))
+
+                        if not match or not smt.mem_exists(topmod, path):
+                            print_msg("Ignoring init value for unknown net: %s" % (name))
+                            continue
+
+                        meminfo = smt.mem_info(topmod, path)
+                        smtexpr = "(select [%s] #b%s)" % (".".join(path), bin(addr)[2:].zfill(meminfo[0]))
+                        width = meminfo[1]
+
+                    else:
+                        smtexpr = "[%s]" % name
+                        width = smt.net_width(topmod, path)
 
                     if width == 1:
                         assert bitidx == 0
-                        smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
+                        smtexpr = "(= %s %s)" % (smtexpr, "true" if value else "false")
                     else:
-                        smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)
+                        smtexpr = "(= ((_ extract %d %d) %s) #b%d)" % (bitidx, bitidx, smtexpr, value)
 
                     constr_assumes[0].append((cexfile, smtexpr))
 
@@ -569,7 +613,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
 
         mems = sorted(smt.hiermems(topmod))
         for mempath in mems:
-            abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+            abits, width, ports = smt.mem_info(topmod, mempath)
             mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
 
             addr_expr_list = list()
@@ -630,7 +674,7 @@ def write_constr_trace(steps_start, steps_stop, index):
 
         mems = sorted(smt.hiermems(topmod))
         for mempath in mems:
-            abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+            abits, width, ports = smt.mem_info(topmod, mempath)
             mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
 
             addr_expr_list = list()
@@ -669,30 +713,40 @@ def write_trace(steps_start, steps_stop, index):
         write_constr_trace(steps_start, steps_stop, index)
 
 
-def print_failed_asserts_worker(mod, state, path):
+def print_failed_asserts_worker(mod, state, path, extrainfo):
     assert mod in smt.modinfo
+    found_failed_assert = False
 
     if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]:
         return
 
     for cellname, celltype in smt.modinfo[mod].cells.items():
-        print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
+        if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo):
+            found_failed_assert = True
 
     for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
         if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
-            print_msg("Assert failed in %s: %s" % (path, assertinfo))
+            print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo))
+            found_failed_assert = True
+
+    return found_failed_assert
 
 
-def print_failed_asserts(state, final=False):
+def print_failed_asserts(state, final=False, extrainfo=""):
     if noinfo: return
     loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
+    found_failed_assert = False
 
     for loc, expr, value in zip(loc_list, expr_list, value_list):
         if smt.bv2int(value) == 0:
-            print_msg("Assert %s failed: %s" % (loc, expr))
+            print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo))
+            found_failed_assert = True
 
     if not final:
-        print_failed_asserts_worker(topmod, "s%d" % state, topmod)
+        if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo):
+            found_failed_assert = True
+
+    return found_failed_assert
 
 
 def print_anyconsts_worker(mod, state, path):
@@ -710,6 +764,24 @@ def print_anyconsts(state):
     print_anyconsts_worker(topmod, "s%d" % state, topmod)
 
 
+def get_cover_list(mod, base):
+    assert mod in smt.modinfo
+
+    cover_expr = list()
+    cover_desc = list()
+
+    for expr, desc in smt.modinfo[mod].covers.items():
+        cover_expr.append("(ite (|%s| %s) #b1 #b0)" % (expr, base))
+        cover_desc.append(desc)
+
+    for cell, submod in smt.modinfo[mod].cells.items():
+        e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base))
+        cover_expr += e
+        cover_desc += d
+
+    return cover_expr, cover_desc
+
+
 if tempind:
     retstatus = False
     skip_counter = step_size
@@ -757,8 +829,92 @@ if tempind:
             retstatus = True
             break
 
+elif covermode:
+    cover_expr, cover_desc = get_cover_list(topmod, "state")
+    cover_mask = "1" * len(cover_desc)
 
-else:  # not tempind
+    if len(cover_expr) > 1:
+        cover_expr = "(concat %s)" % " ".join(cover_expr)
+    elif len(cover_expr) == 1:
+        cover_expr = cover_expr[0]
+    else:
+        cover_expr = "#b0"
+
+    coveridx = 0
+    smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
+
+    step = 0
+    retstatus = False
+    found_failed_assert = False
+
+    assert step_size == 1
+
+    while step < num_steps:
+        smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
+        smt.write("(assert (|%s_u| s%d))" % (topmod, step))
+        smt.write("(assert (|%s_h| s%d))" % (topmod, step))
+        smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
+
+        if step == 0:
+            smt.write("(assert (|%s_i| s0))" % (topmod))
+            smt.write("(assert (|%s_is| s0))" % (topmod))
+
+        else:
+            smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step))
+            smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
+
+        while "1" in cover_mask:
+            print_msg("Checking cover reachability in step %d.." % (step))
+            smt.write("(push 1)")
+            smt.write("(assert (distinct (covers_%d s%d) #b%s))" % (coveridx, step, "0" * len(cover_desc)))
+
+            if smt.check_sat() == "unsat":
+                smt.write("(pop 1)")
+                break
+
+            reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
+            assert len(reached_covers) == len(cover_desc)
+
+            new_cover_mask = []
+
+            for i in range(len(reached_covers)):
+                if reached_covers[i] == "0":
+                    new_cover_mask.append(cover_mask[i])
+                    continue
+
+                print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
+                new_cover_mask.append("0")
+
+            cover_mask = "".join(new_cover_mask)
+
+            for i in range(step+1):
+                if print_failed_asserts(i, extrainfo=" (step %d)" % i):
+                    found_failed_assert = True
+
+            write_trace(0, step+1, "%d" % coveridx)
+
+            if found_failed_assert:
+                break
+
+            coveridx += 1
+            smt.write("(pop 1)")
+            smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask))
+
+        if found_failed_assert:
+            break
+
+        if "1" not in cover_mask:
+            retstatus = True
+            break
+
+        step += 1
+
+    if "1" in cover_mask:
+        for i in range(len(cover_mask)):
+            if cover_mask[i] == "1":
+                print_msg("Unreached cover statement at %s." % cover_desc[i])
+
+else:  # not tempind, covermode
     step = 0
     retstatus = True
     while step < num_steps:

backends/smt2/smtio.py

@@ -42,6 +42,7 @@ class SmtModInfo:
         self.wsize = dict()
         self.cells = dict()
         self.asserts = dict()
+        self.covers = dict()
         self.anyconsts = dict()
 
 
@@ -331,6 +332,9 @@ class SmtIo:
         if fields[1] == "yosys-smt2-assert":
             self.modinfo[self.curmod].asserts[fields[2]] = fields[3]
 
+        if fields[1] == "yosys-smt2-cover":
+            self.modinfo[self.curmod].covers[fields[2]] = fields[3]
+
         if fields[1] == "yosys-smt2-anyconst":
             self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3]
 
@@ -567,6 +571,26 @@ class SmtIo:
         assert net_path[-1] in self.modinfo[mod].wsize
         return self.modinfo[mod].wsize[net_path[-1]]
 
+    def net_exists(self, mod, net_path):
+        for i in range(len(net_path)-1):
+            if mod not in self.modinfo: return False
+            if net_path[i] not in self.modinfo[mod].cells: return False
+            mod = self.modinfo[mod].cells[net_path[i]]
+
+        if mod not in self.modinfo: return False
+        if net_path[-1] not in self.modinfo[mod].wsize: return False
+        return True
+
+    def mem_exists(self, mod, mem_path):
+        for i in range(len(mem_path)-1):
+            if mod not in self.modinfo: return False
+            if mem_path[i] not in self.modinfo[mod].cells: return False
+            mod = self.modinfo[mod].cells[mem_path[i]]
+
+        if mod not in self.modinfo: return False
+        if mem_path[-1] not in self.modinfo[mod].memories: return False
+        return True
+
     def mem_expr(self, mod, base, path, portidx=None, infomode=False):
         if len(path) == 1:
             assert mod in self.modinfo
@@ -582,8 +606,8 @@ class SmtIo:
         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
         return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode)
 
-    def mem_info(self, mod, base, path):
+    def mem_info(self, mod, path):
-        return self.mem_expr(mod, base, path, infomode=True)
+        return self.mem_expr(mod, "", path, infomode=True)
 
     def get_net(self, mod_name, net_path, state_name):
         return self.get(self.net_expr(mod_name, state_name, net_path))

frontends/ast/ast.cc

@@ -84,6 +84,7 @@ std::string AST::type2str(AstNodeType type)
 	X(AST_PREFIX)
 	X(AST_ASSERT)
 	X(AST_ASSUME)
+	X(AST_COVER)
 	X(AST_FCALL)
 	X(AST_TO_BITS)
 	X(AST_TO_SIGNED)

frontends/ast/ast.h

@@ -65,6 +65,7 @@ namespace AST
 		AST_PREFIX,
 		AST_ASSERT,
 		AST_ASSUME,
+		AST_COVER,
 
 		AST_FCALL,
 		AST_TO_BITS,

frontends/ast/genrtlil.cc

@@ -1336,9 +1336,11 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 	// generate $assert cells
 	case AST_ASSERT:
 	case AST_ASSUME:
+	case AST_COVER:
 		{
 			const char *celltype = "$assert";
 			if (type == AST_ASSUME) celltype = "$assume";
+			if (type == AST_COVER) celltype = "$cover";
 
 			log_assert(children.size() == 2);
 

frontends/ast/simplify.cc

@@ -1400,7 +1400,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 	}
 skip_dynamic_range_lvalue_expansion:;
 
-	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && current_block != NULL)
+	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_COVER) && current_block != NULL)
 	{
 		std::stringstream sstr;
 		sstr << "$formal$" << filename << ":" << linenum << "$" << (autoidx++);
@@ -1462,7 +1462,7 @@ skip_dynamic_range_lvalue_expansion:;
 		goto apply_newNode;
 	}
 
-	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && children.size() == 1)
+	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_COVER) && children.size() == 1)
 	{
 		children.push_back(mkconst_int(1, false, 1));
 		did_something = true;

frontends/blif/blifparse.cc

@@ -55,7 +55,30 @@ static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count,
 	}
 }
 
-void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean, bool sop_mode)
+static std::pair<RTLIL::IdString, int> wideports_split(std::string name)
+{
+	int pos = -1;
+
+	if (name.empty() || name.back() != ']')
+		goto failed;
+
+	for (int i = 0; i+1 < GetSize(name); i++) {
+		if (name[i] == '[')
+			pos = i;
+		else if (name[i] < '0' || name[i] > '9')
+			pos = -1;
+		else if (i == pos+1 && name[i] == '0')
+			pos = -1;
+	}
+
+	if (pos >= 0)
+		return std::pair<RTLIL::IdString, int>("\\" + name.substr(0, pos), atoi(name.c_str() + pos+1)+1);
+
+failed:
+	return std::pair<RTLIL::IdString, int>("\\" + name, 0);
+}
+
+void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean, bool sop_mode, bool wideports)
 {
 	RTLIL::Module *module = nullptr;
 	RTLIL::Const *lutptr = NULL;
@@ -96,6 +119,8 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 	dict<RTLIL::IdString, RTLIL::Const> *obj_attributes = nullptr;
 	dict<RTLIL::IdString, RTLIL::Const> *obj_parameters = nullptr;
 
+	dict<RTLIL::IdString, std::pair<int, bool>> wideports_cache;
+
 	size_t buffer_size = 4096;
 	char *buffer = (char*)malloc(buffer_size);
 	int line_count = 0;
@@ -148,7 +173,32 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 
 			if (!strcmp(cmd, ".end"))
 			{
+				for (auto &wp : wideports_cache)
+				{
+					auto name = wp.first;
+					int width = wp.second.first;
+					bool isinput = wp.second.second;
+
+					RTLIL::Wire *wire = module->addWire(name, width);
+					wire->port_input = isinput;
+					wire->port_output = !isinput;
+
+					for (int i = 0; i < width; i++) {
+						RTLIL::IdString other_name = name.str() + stringf("[%d]", i);
+						RTLIL::Wire *other_wire = module->wire(other_name);
+						if (other_wire) {
+							other_wire->port_input = false;
+							other_wire->port_output = false;
+							if (isinput)
+								module->connect(other_wire, SigSpec(wire, i));
+							else
+								module->connect(SigSpec(wire, i), other_wire);
+						}
+					}
+				}
+
 				module->fixup_ports();
+				wideports_cache.clear();
 
 				if (run_clean)
 				{
@@ -187,9 +237,11 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 				continue;
 			}
 
-			if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs")) {
+			if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs"))
+			{
 				char *p;
-				while ((p = strtok(NULL, " \t\r\n")) != NULL) {
+				while ((p = strtok(NULL, " \t\r\n")) != NULL)
+				{
 					RTLIL::IdString wire_name(stringf("\\%s", p));
 					RTLIL::Wire *wire = module->wire(wire_name);
 					if (wire == nullptr)
@@ -198,6 +250,14 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 						wire->port_input = true;
 					else
 						wire->port_output = true;
+
+					if (wideports) {
+						std::pair<RTLIL::IdString, int> wp = wideports_split(p);
+						if (wp.second > 0) {
+							wideports_cache[wp.first].first = std::max(wideports_cache[wp.first].first, wp.second);
+							wideports_cache[wp.first].second = !strcmp(cmd, ".inputs");
+						}
+					}
 				}
 				obj_attributes = nullptr;
 				obj_parameters = nullptr;
@@ -452,6 +512,8 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 		}
 	}
 
+	return;
+
 error:
 	log_error("Syntax error in line %d!\n", line_count);
 }
@@ -469,10 +531,15 @@ struct BlifFrontend : public Frontend {
 		log("    -sop\n");
 		log("        Create $sop cells instead of $lut cells\n");
 		log("\n");
+		log("    -wideports\n");
+		log("        Merge ports that match the pattern 'name[int]' into a single\n");
+		log("        multi-bit port 'name'.\n");
+		log("\n");
 	}
 	virtual void execute(std::istream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 	{
 		bool sop_mode = false;
+		bool wideports = false;
 
 		log_header(design, "Executing BLIF frontend.\n");
 
@@ -483,11 +550,15 @@ struct BlifFrontend : public Frontend {
 				sop_mode = true;
 				continue;
 			}
+			if (arg == "-wideports") {
+				wideports = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
 
-		parse_blif(design, *f, "", true, sop_mode);
+		parse_blif(design, *f, "", true, sop_mode, wideports);
 	}
 } BlifFrontend;
 

frontends/blif/blifparse.h

@@ -24,7 +24,8 @@
 
 YOSYS_NAMESPACE_BEGIN
 
-extern void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean = false, bool sop_mode = false);
+extern void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name,
+		bool run_clean = false, bool sop_mode = false, bool wideports = false);
 
 YOSYS_NAMESPACE_END
 

frontends/verific/build_amd64.txt

@@ -6,7 +6,7 @@ only have the i386 eval version of Verific:
 1.) Use a Makefile.conf like the following one:
 
 --snip--
-CONFIG := clang
+CONFIG := gcc
 ENABLE_TCL := 0
 ENABLE_PLUGINS := 0
 ENABLE_VERIFIC := 1

frontends/verilog/verilog_lexer.l

@@ -177,8 +177,11 @@ YOSYS_NAMESPACE_END
 
 "assert"   { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
 "assume"   { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
+"cover"    { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); }
 "restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
 "property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
+"rand"     { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); }
+"const"    { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); }
 "logic"    { SV_KEYWORD(TOK_REG); }
 "bit"      { SV_KEYWORD(TOK_REG); }
 
@@ -192,14 +195,17 @@ YOSYS_NAMESPACE_END
 "genvar"  { return TOK_GENVAR; }
 "real"    { return TOK_REAL; }
 
+"enum"    { SV_KEYWORD(TOK_ENUM); }
+"typedef" { SV_KEYWORD(TOK_TYPEDEF); }
+
 [0-9][0-9_]* {
 	frontend_verilog_yylval.string = new std::string(yytext);
-	return TOK_CONST;
+	return TOK_CONSTVAL;
 }
 
 [0-9]*[ \t]*\'s?[bodhBODH][ \t\r\n]*[0-9a-fA-FzxZX?_]+ {
 	frontend_verilog_yylval.string = new std::string(yytext);
-	return TOK_CONST;
+	return TOK_CONSTVAL;
 }
 
 [0-9][0-9_]*\.[0-9][0-9_]*([eE][-+]?[0-9_]+)? {

frontends/verilog/verilog_parser.y

@@ -59,6 +59,7 @@ namespace VERILOG_FRONTEND {
 	bool default_nettype_wire;
 	bool sv_mode, formal_mode, lib_mode;
 	bool norestrict_mode, assume_asserts_mode;
+	bool current_wire_rand, current_wire_const;
 	std::istream *lexin;
 }
 YOSYS_NAMESPACE_END
@@ -100,7 +101,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 	bool boolean;
 }
 
-%token <string> TOK_STRING TOK_ID TOK_CONST TOK_REALVAL TOK_PRIMITIVE
+%token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE
 %token ATTR_BEGIN ATTR_END DEFATTR_BEGIN DEFATTR_END
 %token TOK_MODULE TOK_ENDMODULE TOK_PARAMETER TOK_LOCALPARAM TOK_DEFPARAM
 %token TOK_PACKAGE TOK_ENDPACKAGE TOK_PACKAGESEP
@@ -114,7 +115,8 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
 %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
-%token TOK_RESTRICT TOK_PROPERTY
+%token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
+%token TOK_RAND TOK_CONST
 
 %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
@@ -355,6 +357,8 @@ delay:
 wire_type:
 	{
 		astbuf3 = new AstNode(AST_WIRE);
+		current_wire_rand = false;
+		current_wire_const = false;
 	} wire_type_token_list delay {
 		$$ = astbuf3;
 	};
@@ -392,6 +396,12 @@ wire_type_token:
 	} |
 	TOK_SIGNED {
 		astbuf3->is_signed = true;
+	} |
+	TOK_RAND {
+		current_wire_rand = true;
+	} |
+	TOK_CONST {
+		current_wire_const = true;
 	};
 
 non_opt_range:
@@ -730,7 +740,15 @@ wire_name_list:
 	wire_name_and_opt_assign | wire_name_list ',' wire_name_and_opt_assign;
 
 wire_name_and_opt_assign:
-	wire_name |
+	wire_name {
+		if (current_wire_rand) {
+			AstNode *wire = new AstNode(AST_IDENTIFIER);
+			AstNode *fcall = new AstNode(AST_FCALL);
+			wire->str = ast_stack.back()->children.back()->str;
+			fcall->str = current_wire_const ? "\\$anyconst" : "\\$anyseq";
+			ast_stack.back()->children.push_back(new AstNode(AST_ASSIGN, wire, fcall));
+		}
+	} |
 	wire_name '=' expr {
 		AstNode *wire = new AstNode(AST_IDENTIFIER);
 		wire->str = ast_stack.back()->children.back()->str;
@@ -1000,6 +1018,15 @@ assert:
 	TOK_ASSUME '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3));
 	} |
+	TOK_COVER '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $3));
+	} |
+	TOK_COVER '(' ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	} |
+	TOK_COVER ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	} |
 	TOK_RESTRICT '(' expr ')' ';' {
 		if (norestrict_mode)
 			delete $3;
@@ -1014,6 +1041,9 @@ assert_property:
 	TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
 	} |
+	TOK_COVER TOK_PROPERTY '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $4));
+	} |
 	TOK_RESTRICT TOK_PROPERTY '(' expr ')' ';' {
 		if (norestrict_mode)
 			delete $4;
@@ -1350,7 +1380,7 @@ basic_expr:
 	rvalue {
 		$$ = $1;
 	} |
-	'(' expr ')' TOK_CONST {
+	'(' expr ')' TOK_CONSTVAL {
 		if ($4->substr(0, 1) != "'")
 			frontend_verilog_yyerror("Syntax error.");
 		AstNode *bits = $2;
@@ -1360,7 +1390,7 @@ basic_expr:
 		$$ = new AstNode(AST_TO_BITS, bits, val);
 		delete $4;
 	} |
-	hierarchical_id TOK_CONST {
+	hierarchical_id TOK_CONSTVAL {
 		if ($2->substr(0, 1) != "'")
 			frontend_verilog_yyerror("Syntax error.");
 		AstNode *bits = new AstNode(AST_IDENTIFIER);
@@ -1372,14 +1402,14 @@ basic_expr:
 		delete $1;
 		delete $2;
 	} |
-	TOK_CONST TOK_CONST {
+	TOK_CONSTVAL TOK_CONSTVAL {
 		$$ = const2ast(*$1 + *$2, case_type_stack.size() == 0 ? 0 : case_type_stack.back(), !lib_mode);
 		if ($$ == NULL || (*$2)[0] != '\'')
 			log_error("Value conversion failed: `%s%s'\n", $1->c_str(), $2->c_str());
 		delete $1;
 		delete $2;
 	} |
-	TOK_CONST {
+	TOK_CONSTVAL {
 		$$ = const2ast(*$1, case_type_stack.size() == 0 ? 0 : case_type_stack.back(), !lib_mode);
 		if ($$ == NULL)
 			log_error("Value conversion failed: `%s'\n", $1->c_str());

kernel/celltypes.h

@@ -116,6 +116,7 @@ struct CellTypes
 
 		setup_type("$assert", {A, EN}, pool<RTLIL::IdString>(), true);
 		setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true);
+		setup_type("$cover", {A, EN}, pool<RTLIL::IdString>(), true);
 		setup_type("$initstate", pool<RTLIL::IdString>(), {Y}, true);
 		setup_type("$anyconst", pool<RTLIL::IdString>(), {Y}, true);
 		setup_type("$anyseq", pool<RTLIL::IdString>(), {Y}, true);

kernel/rtlil.cc

@@ -1026,7 +1026,7 @@ namespace {
 				return;
 			}
 
-			if (cell->type.in("$assert", "$assume")) {
+			if (cell->type.in("$assert", "$assume", "$cover")) {
 				port("\\A", 1);
 				port("\\EN", 1);
 				check_expected();
@@ -1819,6 +1819,14 @@ RTLIL::Cell* RTLIL::Module::addAssume(RTLIL::IdString name, RTLIL::SigSpec sig_a
 	return cell;
 }
 
+RTLIL::Cell* RTLIL::Module::addCover(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en)
+{
+	RTLIL::Cell *cell = addCell(name, "$cover");
+	cell->setPort("\\A", sig_a);
+	cell->setPort("\\EN", sig_en);
+	return cell;
+}
+
 RTLIL::Cell* RTLIL::Module::addEquiv(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y)
 {
 	RTLIL::Cell *cell = addCell(name, "$equiv");
@@ -2050,6 +2058,7 @@ RTLIL::Memory::Memory()
 	hashidx_ = hashidx_count;
 
 	width = 1;
+	start_offset = 0;
 	size = 0;
 }
 

kernel/rtlil.h

@@ -1007,6 +1007,7 @@ public:
 	RTLIL::Cell* addTribuf (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_y);
 	RTLIL::Cell* addAssert (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en);
 	RTLIL::Cell* addAssume (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en);
+	RTLIL::Cell* addCover  (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en);
 	RTLIL::Cell* addEquiv  (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y);
 
 	RTLIL::Cell* addSr    (RTLIL::IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, RTLIL::SigSpec sig_q, bool set_polarity = true, bool clr_polarity = true);

kernel/satgen.h

@@ -507,11 +507,7 @@ struct SatGen
 				std::vector<int> undef_s = importUndefSigSpec(cell->getPort("\\S"), timestep);
 				std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
 
-				int maybe_one_hot = ez->CONST_FALSE;
+				int maybe_a = ez->CONST_TRUE;
-				int maybe_many_hot = ez->CONST_FALSE;
-
-				int sure_one_hot = ez->CONST_FALSE;
-				int sure_many_hot = ez->CONST_FALSE;
 
 				std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
 				std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
@@ -524,18 +520,12 @@ struct SatGen
 					int maybe_s = ez->OR(s.at(i), undef_s.at(i));
 					int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i)));
 
-					maybe_one_hot = ez->OR(maybe_one_hot, maybe_s);
+					maybe_a = ez->AND(maybe_a, ez->NOT(sure_s));
-					maybe_many_hot = ez->OR(maybe_many_hot, ez->AND(maybe_one_hot, maybe_s));
 
-					sure_one_hot = ez->OR(sure_one_hot, sure_s);
+					bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set);
-					sure_many_hot = ez->OR(sure_many_hot, ez->AND(sure_one_hot, sure_s));
+					bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr);
-
-					bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b))), bits_set);
-					bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b))), bits_clr);
 				}
 
-				int maybe_a = ez->NOT(maybe_one_hot);
-
 				bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set);
 				bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr);
 

manual/CHAPTER_CellLib.tex

@@ -421,7 +421,7 @@ pass. The combinatorial logic cells can be mapped to physical cells from a Liber
 using the {\tt abc} pass.
 
 \begin{fixme}
-Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$anyconst}, and {\tt \$anyseq} cells.
+Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$cover}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$anyconst}, and {\tt \$anyseq} cells.
 \end{fixme}
 
 \begin{fixme}

manual/clean.sh

@@ -1,2 +1,2 @@
 #!/bin/bash
-for f in $( find . -name .gitignore ); do sed -re "s,^,find ${f%.gitignore} -name ',; s,$,' | xargs rm -f,;" $f; done | bash -v
+for f in $( find . -name .gitignore ); do sed -Ee "s,^,find ${f%.gitignore} -name ',; s,$,' | xargs rm -f,;" $f; done | bash -v

passes/equiv/equiv_simple.cc

@@ -59,7 +59,7 @@ struct EquivSimpleWorker
 		for (auto &conn : cell->connections())
 			if (yosys_celltypes.cell_input(cell->type, conn.first))
 				for (auto bit : sigmap(conn.second)) {
-					if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_")) {
+					if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_")) {
 						if (!conn.first.in("\\CLK", "\\C"))
 							next_seed.insert(bit);
 					} else
@@ -329,7 +329,7 @@ struct EquivSimplePass : public Pass {
 					unproven_cells_counter, GetSize(unproven_equiv_cells), log_id(module));
 
 			for (auto cell : module->cells()) {
-				if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_"))
+				if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_"))
 					continue;
 				for (auto &conn : cell->connections())
 					if (yosys_celltypes.cell_output(cell->type, conn.first))

passes/fsm/fsm_expand.cc

@@ -54,13 +54,27 @@ struct FsmExpand
 			if (cell->getPort("\\A").size() < 2)
 				return true;
 
+		int in_bits = 0;
 		RTLIL::SigSpec new_signals;
-		if (cell->hasPort("\\A"))
+
+		if (cell->hasPort("\\A")) {
+			in_bits += GetSize(cell->getPort("\\A"));
 			new_signals.append(assign_map(cell->getPort("\\A")));
-		if (cell->hasPort("\\B"))
+		}
+
+		if (cell->hasPort("\\B")) {
+			in_bits += GetSize(cell->getPort("\\B"));
 			new_signals.append(assign_map(cell->getPort("\\B")));
-		if (cell->hasPort("\\S"))
+		}
+
+		if (cell->hasPort("\\S")) {
+			in_bits += GetSize(cell->getPort("\\S"));
 			new_signals.append(assign_map(cell->getPort("\\S")));
+		}
+
+		if (in_bits > 8)
+			return false;
+
 		if (cell->hasPort("\\Y"))
 			new_signals.append(assign_map(cell->getPort("\\Y")));
 
@@ -173,6 +187,16 @@ struct FsmExpand
 		new_ctrl_out.append(output_sig);
 		fsm_cell->setPort("\\CTRL_OUT", new_ctrl_out);
 
+		if (GetSize(input_sig) > 10)
+			log_warning("Cell %s.%s (%s) has %d input bits, merging into FSM %s.%s might be problematic.\n",
+					log_id(cell->module), log_id(cell), log_id(cell->type),
+					GetSize(input_sig), log_id(fsm_cell->module), log_id(fsm_cell));
+
+		if (GetSize(fsm_data.transition_table) > 10000)
+			log_warning("Transition table for FSM %s.%s already has %d rows, merging more cells "
+					"into this FSM might be problematic.\n", log_id(fsm_cell->module), log_id(fsm_cell),
+					GetSize(fsm_data.transition_table));
+
 		std::vector<FsmData::transition_t> new_transition_table;
 		for (auto &tr : fsm_data.transition_table) {
 			for (int i = 0; i < (1 << input_sig.size()); i++) {

passes/hierarchy/hierarchy.cc

@@ -175,16 +175,12 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
 			{
 				filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".v";
 				if (check_file_exists(filename)) {
-					std::vector<std::string> args;
-					args.push_back(filename);
 					Frontend::frontend_call(design, NULL, filename, "verilog");
 					goto loaded_module;
 				}
 
 				filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".il";
 				if (check_file_exists(filename)) {
-					std::vector<std::string> args;
-					args.push_back(filename);
 					Frontend::frontend_call(design, NULL, filename, "ilang");
 					goto loaded_module;
 				}
@@ -317,7 +313,7 @@ bool set_keep_assert(std::map<RTLIL::Module*, bool> &cache, RTLIL::Module *mod)
 	if (cache.count(mod) == 0)
 		for (auto c : mod->cells()) {
 			RTLIL::Module *m = mod->design->module(c->type);
-			if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in("$assert", "$assume"))
+			if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in("$assert", "$assume", "$cover"))
 				return cache[mod] = true;
 		}
 	return cache[mod];

passes/opt/opt_clean.cc

@@ -64,7 +64,7 @@ struct keep_cache_t
 
 	bool query(Cell *cell)
 	{
-		if (cell->type.in("$memwr", "$meminit", "$assert", "$assume"))
+		if (cell->type.in("$memwr", "$meminit", "$assert", "$assume", "$cover"))
 			return true;
 
 		if (cell->has_keep_attr())

passes/opt/opt_expr.cc

@@ -259,6 +259,29 @@ bool is_one_or_minus_one(const Const &value, bool is_signed, bool &is_negative)
 	return last_bit_one;
 }
 
+// if the signal has only one bit set, return the index of that bit.
+// otherwise return -1
+int get_onehot_bit_index(RTLIL::SigSpec signal)
+{
+	int bit_index = -1;
+
+	for (int i = 0; i < GetSize(signal); i++)
+	{
+		if (signal[i] == RTLIL::State::S0)
+			continue;
+
+		if (signal[i] != RTLIL::State::S1)
+			return -1;
+
+		if (bit_index != -1)
+			return -1;
+
+		bit_index = i;
+	}
+
+	return bit_index;
+}
+
 void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool consume_x, bool mux_undef, bool mux_bool, bool do_fine, bool keepdc, bool clkinv)
 {
 	if (!design->selected(module))
@@ -1167,6 +1190,103 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 			}
 		}
 
+		// replace a<0 or a>=0 with the top bit of a
+		if (do_fine && (cell->type == "$lt" || cell->type == "$ge" || cell->type == "$gt" || cell->type == "$le"))
+		{
+			//used to decide whether the signal needs to be negated
+			bool is_lt = false;
+
+			//references the variable signal in the comparison
+			RTLIL::SigSpec sigVar;
+
+			//references the constant signal in the comparison
+			RTLIL::SigSpec sigConst;
+
+			// note that this signal must be constant for the optimization 
+			// to take place, but it is not checked beforehand.
+			// If new passes are added, this signal must be checked for const-ness
+
+			//width of the variable port
+			int width;
+
+			bool var_signed;
+
+			if (cell->type == "$lt" || cell->type == "$ge") {
+				is_lt = cell->type == "$lt" ? 1 : 0;
+				sigVar = cell->getPort("\\A");
+				sigConst = cell->getPort("\\B");
+				width = cell->parameters["\\A_WIDTH"].as_int();
+				var_signed = cell->parameters["\\A_SIGNED"].as_bool();
+			} else
+			if (cell->type == "$gt" || cell->type == "$le") {
+				is_lt = cell->type == "$gt" ? 1 : 0;
+				sigVar = cell->getPort("\\B");
+				sigConst = cell->getPort("\\A");
+				width = cell->parameters["\\B_WIDTH"].as_int();
+				var_signed = cell->parameters["\\B_SIGNED"].as_bool();
+			}
+
+			// replace a(signed) < 0 with the high bit of a
+			if (sigConst.is_fully_const() && sigConst.is_fully_zero() && var_signed == true)
+			{
+				RTLIL::SigSpec a_prime(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int());
+				a_prime[0] = sigVar[width - 1];
+				if (is_lt) {
+					log("Replacing %s cell `%s' (implementing X<0) with X[%d]: %s\n",
+							log_id(cell->type), log_id(cell), width-1, log_signal(a_prime));
+					module->connect(cell->getPort("\\Y"), a_prime);
+					module->remove(cell);
+				} else {
+					log("Replacing %s cell `%s' (implementing X>=0) with ~X[%d]: %s\n",
+							log_id(cell->type), log_id(cell), width-1, log_signal(a_prime));
+					module->addNot(NEW_ID, a_prime, cell->getPort("\\Y"));
+					module->remove(cell);
+				}
+				did_something = true;
+				goto next_cell;
+			} else
+			if (sigConst.is_fully_const() && sigConst.is_fully_def() && var_signed == false)
+			{
+				if (sigConst.is_fully_zero()) {
+					RTLIL::SigSpec a_prime(RTLIL::State::S0, 1);
+					if (is_lt) {
+						log("Replacing %s cell `%s' (implementing unsigned X<0) with constant false.\n",
+								log_id(cell->type), log_id(cell));
+						a_prime[0] = RTLIL::State::S0;
+					} else {
+						log("Replacing %s cell `%s' (implementing unsigned X>=0) with constant true.\n",
+								log_id(cell->type), log_id(cell));
+						a_prime[0] = RTLIL::State::S1;
+					}
+					module->connect(cell->getPort("\\Y"), a_prime);
+					module->remove(cell);
+					did_something = true;
+					goto next_cell;
+				}
+
+				int const_bit_set = get_onehot_bit_index(sigConst);
+				if (const_bit_set >= 0) {
+					int bit_set = const_bit_set;
+					RTLIL::SigSpec a_prime(RTLIL::State::S0, width - bit_set);
+					for (int i = bit_set; i < width; i++) {
+						a_prime[i - bit_set] = sigVar[i];
+					}
+					if (is_lt) {
+						log("Replacing %s cell `%s' (implementing unsigned X<%s) with !X[%d:%d]: %s.\n",
+								log_id(cell->type), log_id(cell), log_signal(sigConst), width - 1, bit_set, log_signal(a_prime));
+						module->addLogicNot(NEW_ID, a_prime, cell->getPort("\\Y"));
+					} else {
+						log("Replacing %s cell `%s' (implementing unsigned X>=%s) with |X[%d:%d]: %s.\n",
+								log_id(cell->type), log_id(cell), log_signal(sigConst), width - 1, bit_set, log_signal(a_prime));
+						module->addReduceOr(NEW_ID, a_prime, cell->getPort("\\Y"));
+					}
+					module->remove(cell);
+					did_something = true;
+					goto next_cell;
+				}
+			}
+		}
+
 	next_cell:;
 #undef ACTION_DO
 #undef ACTION_DO_Y

passes/opt/opt_rmdff.cc

@@ -41,9 +41,27 @@ void remove_init_attr(SigSpec sig)
 
 bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch)
 {
-	SigSpec sig_e = dlatch->getPort("\\EN");
+	SigSpec sig_e;
+	State on_state, off_state;
 
-	if (sig_e == State::S0)
+	if (dlatch->type == "$dlatch") {
+		sig_e = assign_map(dlatch->getPort("\\EN"));
+		on_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S1 : State::S0;
+		off_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S0 : State::S1;
+	} else
+	if (dlatch->type == "$_DLATCH_P_") {
+		sig_e = assign_map(dlatch->getPort("\\E"));
+		on_state = State::S1;
+		off_state = State::S0;
+	} else
+	if (dlatch->type == "$_DLATCH_N_") {
+		sig_e = assign_map(dlatch->getPort("\\E"));
+		on_state = State::S0;
+		off_state = State::S1;
+	} else
+		log_abort();
+
+	if (sig_e == off_state)
 	{
 		RTLIL::Const val_init;
 		for (auto bit : dff_init_map(dlatch->getPort("\\Q")))
@@ -52,7 +70,7 @@ bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch)
 		goto delete_dlatch;
 	}
 
-	if (sig_e == State::S1)
+	if (sig_e == on_state)
 	{
 		mod->connect(dlatch->getPort("\\Q"), dlatch->getPort("\\D"));
 		goto delete_dlatch;
@@ -268,7 +286,7 @@ struct OptRmdffPass : public Pass {
 						"$ff", "$dff", "$adff"))
 					dff_list.push_back(cell->name);
 
-				if (cell->type == "$dlatch")
+				if (cell->type.in("$dlatch", "$_DLATCH_P_", "$_DLATCH_N_"))
 					dlatch_list.push_back(cell->name);
 			}
 

passes/techmap/abc.cc

@@ -29,11 +29,11 @@
 // Kahn, Arthur B. (1962), "Topological sorting of large networks", Communications of the ACM 5 (11): 558-562, doi:10.1145/368996.369025
 // http://en.wikipedia.org/wiki/Topological_sorting
 
-#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map {D}"
+#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put"
-#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"
+#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p"
 #define ABC_COMMAND_LUT "strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2"
 #define ABC_COMMAND_SOP "strash; ifraig; scorr; dc2; dretime; strash; dch -f; cover {I} {P}"
-#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map"
+#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put"
 
 #define ABC_FAST_COMMAND_LIB "strash; dretime; map {D}"
 #define ABC_FAST_COMMAND_CTR "strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"

techlibs/common/simlib.v

@@ -1305,6 +1305,14 @@ endmodule
 
 // --------------------------------------------------------
 
+module \$cover (A, EN);
+
+input A, EN;
+
+endmodule
+
+// --------------------------------------------------------
+
 module \$initstate (Y);
 
 output reg Y = 1;