diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 15 | ||||
| -rw-r--r-- | passes/techmap/dfflibmap.cc | 11 |
3 files changed, 23 insertions, 5 deletions
@@ -109,7 +109,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 = 14d985a +ABCREV = 4d56acf ABCPULL = 1 ABCURL ?= https://github.com/berkeley-abc/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index afbcf1fc4..68783e744 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -166,19 +166,28 @@ class SmtIo: self.unroll = False if self.solver == "yices": - self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['yices-smt2'] + self.solver_opts + else: + 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.6' if self.logic_dt else 'smt2'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts + else: + 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 if self.solver == "boolector": - self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts + if self.noincr: + self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts + else: + self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts self.unroll = True if self.solver == "abc": diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 421073485..b0528d473 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -101,7 +101,16 @@ static bool parse_pin(LibertyAst *cell, LibertyAst *attr, std::string &pin_name, if (child->id == "pin" && child->args.size() == 1 && child->args[0] == pin_name) return true; - log_error("Malformed liberty file - cannot find pin '%s' in cell '%s'.\n", pin_name.c_str(), cell->args[0].c_str()); + /* If we end up here, the pin specified in the attribute does not exist, which is an error, + or, the attribute contains an expression which we do not yet support. + For now, we'll simply produce a warning to let the user know something is up. + */ + if (pin_name.find_first_of("^*|&") == std::string::npos) { + log_warning("Malformed liberty file - cannot find pin '%s' in cell '%s' - skipping.\n", pin_name.c_str(), cell->args[0].c_str()); + } + else { + log_warning("Found unsupported expression '%s' in pin attribute of cell '%s' - skipping.\n", pin_name.c_str(), cell->args[0].c_str()); + } return false; } |