Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: azonenberg/yosys
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: d6feb4b43e60
Choose a base ref
...
head repository: azonenberg/yosys
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 2effa497a332
Choose a head ref
  • 6 commits
  • 4 files changed
  • 2 contributors

Commits on Oct 17, 2016

  1. Copy the full SHA
    6425d34 View commit details
  2. Copy the full SHA
    15fb566 View commit details
  3. Copy the full SHA
    0bcc617 View commit details

Commits on Oct 18, 2016

  1. Verified

    This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
    Copy the full SHA
    9e980a2 View commit details
  2. Copy the full SHA
    281a977 View commit details

Commits on Oct 19, 2016

  1. Copy the full SHA
    2effa49 View commit details
Showing with 98 additions and 8 deletions.
  1. +1 −4 backends/blif/blif.cc
  2. +38 −1 backends/smt2/smtbmc.py
  3. +57 −1 passes/sat/clk2fflogic.cc
  4. +2 −2 passes/sat/miter.cc
5 changes: 1 addition & 4 deletions backends/blif/blif.cc
Original file line number Diff line number Diff line change
@@ -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));

39 changes: 38 additions & 1 deletion backends/smt2/smtbmc.py
Original file line number Diff line number Diff line change
@@ -26,6 +26,7 @@
step_size = 1
num_steps = 20
vcdfile = None
cexfile = None
vlogtbfile = None
inconstr = list()
outconstr = None
@@ -61,6 +62,9 @@ def usage():
--smtc <constr_filename>
read constraints file
--cex <cex_filename>
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 @@ def usage():

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 @@ def usage():
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,37 @@ def print_msg(msg):
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, 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

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)
58 changes: 57 additions & 1 deletion passes/sat/clk2fflogic.cc
Original file line number Diff line number Diff line change
@@ -72,7 +72,47 @@ struct Clk2fflogicPass : public Pass {

for (auto cell : vector<Cell*>(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);
}
4 changes: 2 additions & 2 deletions passes/sat/miter.cc
Original file line number Diff line number Diff line change
@@ -338,12 +338,12 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> 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);