diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 14 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 10 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 12 |
3 files changed, 21 insertions, 15 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 8be9e05f1..a928419a1 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1,7 +1,7 @@ /* * yosys -- Yosys Open SYnthesis Suite * - * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> + * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com> * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above @@ -124,6 +124,7 @@ struct Smt2Worker memories = Mem::get_all_memories(module); for (auto &mem : memories) { + mem.narrow(); mem_dict[mem.memid] = &mem; for (auto &port : mem.wr_ports) { @@ -182,7 +183,7 @@ struct Smt2Worker continue; // Handled above. - if (cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) { + if (cell->is_mem_cell()) { mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()]; continue; } @@ -694,7 +695,7 @@ struct Smt2Worker // FIXME: $slice $concat } - if (memmode && cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) + if (memmode && cell->is_mem_cell()) { Mem *mem = mem_cells[cell]; @@ -859,7 +860,7 @@ struct Smt2Worker log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smt2`.\n", log_id(cell->type), log_id(module), log_id(cell)); } - if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") { + if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") { log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smt2`.\n", log_id(cell->type), log_id(module), log_id(cell)); } @@ -1530,6 +1531,11 @@ struct Smt2Backend : public Backend { log_header(design, "Executing SMT2 backend.\n"); + log_push(); + Pass::call(design, "bmuxmap"); + Pass::call(design, "demuxmap"); + log_pop(); + size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index da5a7f57e..e5cfcdc08 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -2,7 +2,7 @@ # # yosys -- Yosys Open SYnthesis Suite # -# Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> +# Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com> # # Permission to use, copy, modify, and/or distribute this software for any # purpose with or without fee is hereby granted, provided that the above @@ -771,12 +771,12 @@ def write_vcd_trace(steps_start, steps_stop, index): if gotread: buf = data[:] - for i in reversed(range(len(tdata))): + for ii in reversed(range(len(tdata))): for k in range(width): - if tdata[i][k] == "x": - tdata[i][k] = buf[k] + if tdata[ii][k] == "x": + tdata[ii][k] = buf[k] else: - buf[k] = tdata[i][k] + buf[k] = tdata[ii][k] if not asyncwr: tdata.append(data[:]) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 516091011..d73a875ba 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -1,7 +1,7 @@ # # yosys -- Yosys Open SYnthesis Suite # -# Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> +# Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com> # # Permission to use, copy, modify, and/or distribute this software for any # purpose with or without fee is hereby granted, provided that the above @@ -203,14 +203,14 @@ class SmtIo: print('timeout option is not supported for mathsat.') sys.exit(1) - if self.solver == "boolector": + if self.solver in ["boolector", "bitwuzla"]: if self.noincr: - self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts + self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts else: - self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts + self.popen_vargs = [self.solver, '--smt2', '-i'] + self.solver_opts self.unroll = True if self.timeout != 0: - print('timeout option is not supported for boolector.') + print('timeout option is not supported for %s.' % self.solver) sys.exit(1) if self.solver == "abc": @@ -1010,7 +1010,7 @@ class SmtOpts: def helpmsg(self): return """ -s <solver> - set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy + set SMT solver: z3, yices, boolector, bitwuzla, cvc4, mathsat, dummy default: yices -S <opt> |