From 6425d34e73914f98bcd355a41700651edab1eb93 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 17 Oct 2016 13:28:55 +0200 Subject: [PATCH 1/5] Added clk2fflogic support for $dffsr and $dlatch --- passes/sat/clk2fflogic.cc | 58 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 57 insertions(+), 1 deletion(-) diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index 301d3e78..ef6d5dd7 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -72,7 +72,47 @@ struct Clk2fflogicPass : public Pass { for (auto cell : vector(module->selected_cells())) { - if (cell->type.in("$dff", "$adff")) + if (cell->type.in("$dlatch")) + { + bool enpol = cell->parameters["\\EN_POLARITY"].as_bool(); + + SigSpec sig_en = cell->getPort("\\EN"); + SigSpec sig_d = cell->getPort("\\D"); + SigSpec sig_q = cell->getPort("\\Q"); + + log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(sig_en), log_signal(sig_d), log_signal(sig_q)); + + Wire *past_q = module->addWire(NEW_ID, GetSize(sig_q)); + module->addFf(NEW_ID, sig_q, past_q); + + if (enpol) + module->addMux(NEW_ID, past_q, sig_d, sig_en, sig_q); + else + module->addMux(NEW_ID, sig_d, past_q, sig_en, sig_q); + + Const initval; + bool assign_initval = false; + for (int i = 0; i < GetSize(sig_d); i++) { + SigBit qbit = sigmap(sig_q[i]); + if (initbits.count(qbit)) { + initval.bits.push_back(initbits.at(qbit)); + del_initbits.insert(qbit); + } else + initval.bits.push_back(State::Sx); + if (initval.bits.back() != State::Sx) + assign_initval = true; + } + + if (assign_initval) + past_q->attributes["\\init"] = initval; + + module->remove(cell); + continue; + } + + if (cell->type.in("$dff", "$adff", "$dffsr")) { bool clkpol = cell->parameters["\\CLK_POLARITY"].as_bool(); @@ -117,6 +157,22 @@ struct Clk2fflogicPass : public Pass { module->addMux(NEW_ID, rstval, qval, arst, sig_q); } else + if (cell->type == "$dffsr") + { + SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); + SigSpec setval = cell->getPort("\\SET"); + SigSpec clrval = cell->getPort("\\CLR"); + + if (!cell->parameters["\\SET_POLARITY"].as_bool()) + setval = module->Not(NEW_ID, setval); + + if (cell->parameters["\\CLR_POLARITY"].as_bool()) + clrval = module->Not(NEW_ID, clrval); + + qval = module->Or(NEW_ID, qval, setval); + module->addAnd(NEW_ID, qval, clrval, sig_q); + } + else { module->addMux(NEW_ID, past_q, past_d, clock_edge, sig_q); } From 15fb56697a7ecf5378ffbb0e6ea8716ceddb1809 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 17 Oct 2016 14:56:58 +0200 Subject: [PATCH 2/5] Bugfix in "miter -assert" handling of assumptions --- passes/sat/miter.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc index 341a6bac..9e150b60 100644 --- a/passes/sat/miter.cc +++ b/passes/sat/miter.cc @@ -338,12 +338,12 @@ void create_miter_assert(struct Pass *that, std::vector args, RTLIL else { Wire *assume_q = module->addWire(NEW_ID); - assume_q->attributes["\\init"] = State::S1; + assume_q->attributes["\\init"] = State::S0; assume_signals.append(assume_q); SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals); SigSpec assume_ok = module->Not(NEW_ID, assume_nok); - module->addFf(NEW_ID, assume_ok, assume_q); + module->addFf(NEW_ID, assume_nok, assume_q); SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals); module->addAnd(NEW_ID, assert_fail, assume_ok, trigger); From 0bcc617a4f01d5810965e65b7a8d5013913175e7 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 17 Oct 2016 14:57:28 +0200 Subject: [PATCH 3/5] Added "yosys-smtbmc --cex " --- backends/smt2/smtbmc.py | 36 +++++++++++++++++++++++++++++++++++- 1 file changed, 35 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 0cfb386a..fabcdc92 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -26,6 +26,7 @@ skip_steps = 0 step_size = 1 num_steps = 20 vcdfile = None +cexfile = None vlogtbfile = None inconstr = list() outconstr = None @@ -61,6 +62,9 @@ yosys-smtbmc [options] --smtc read constraints file + --cex + read cex file as written by ABC's "write_cex -n" + --noinfo only run the core proof, do not collect and print any additional information (e.g. which assert failed) @@ -94,7 +98,7 @@ yosys-smtbmc [options] try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts + - ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"]) + ["final-only", "assume-skipped=", "smtc=", "cex=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"]) except: usage() @@ -118,6 +122,8 @@ for o, a in opts: final_only = True elif o == "--smtc": inconstr.append(a) + elif o == "--cex": + cexfile = a elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -311,6 +317,34 @@ if topmod is None: assert topmod is not None assert topmod in smt.modinfo +if cexfile is not None: + with open(cexfile, "r") as f: + cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?(@\d+)=([01])') + for entry in f.read().split(): + match = cex_regex.match(entry) + assert match + + name, bit, step, val = match.group(1), match.group(2), match.group(3), match.group(4) + + if name not in smt.modinfo[topmod].inputs: + continue + + if bit is None: + bit = 0 + else: + bit = int(bit[1:-1]) + + step = int(step[1:]) + val = int(val) + + if smt.modinfo[topmod].wsize[name] == 1: + assert bit == 0 + smtexpr = "(= [%s] %s)" % (name, "true" if val else "false") + else: + smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bit, bit, name, val) + + # print("cex@%d: %s" % (step, smtexpr)) + constr_assumes[step].append((cexfile, smtexpr)) def write_vcd_trace(steps_start, steps_stop, index): filename = vcdfile.replace("%", index) From 9e980a2bb0c0595a4310c4c450b9a2c28c6ad9ed Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 18 Oct 2016 10:54:04 +0200 Subject: [PATCH 4/5] Use init value "2" for all uninitialized FFs in BLIF back-end --- backends/blif/blif.cc | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc index 0dc17c92..d9d0cc17 100644 --- a/backends/blif/blif.cc +++ b/backends/blif/blif.cc @@ -77,9 +77,6 @@ struct BlifDumper case State::S1: init_bits[initsig[i]] = 1; break; - case State::Sx: - init_bits[initsig[i]] = 2; - break; default: break; } @@ -126,7 +123,7 @@ struct BlifDumper sigmap.apply(sig); if (init_bits.count(sig) == 0) - return ""; + return " 2"; string str = stringf(" %d", init_bits.at(sig)); From 281a977b39ec832b5ad4d84027dc98a6e8f99d7c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 18 Oct 2016 10:54:53 +0200 Subject: [PATCH 5/5] Ignore L_pi nets in "yosys-smtbmc --cex" --- backends/smt2/smtbmc.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index fabcdc92..04c25f91 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -319,12 +319,15 @@ assert topmod in smt.modinfo if cexfile is not None: with open(cexfile, "r") as f: - cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?(@\d+)=([01])') + cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])') for entry in f.read().split(): match = cex_regex.match(entry) assert match - name, bit, step, val = match.group(1), match.group(2), match.group(3), match.group(4) + name, bit, extra_name, step, val = match.group(1), match.group(2), match.group(3), match.group(4), match.group(5) + + if extra_name != "": + continue if name not in smt.modinfo[topmod].inputs: continue