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: fad52abf70a0
Choose a base ref
...
head repository: azonenberg/yosys
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 05df3dbee434
Choose a head ref
  • 3 commits
  • 5 files changed
  • 1 contributor

Commits on May 27, 2017

  1. Change default smt2 solver to yices (Yices 2 has switched its license… 

    … to GPL)
    @cliffordwolf
    cliffordwolf committed May 27, 2017
    Copy the full SHA
    d9201b8 View commit details

Commits on May 28, 2017

  1. Improve write_aiger handling of unconnected nets and constants

    @cliffordwolf
    cliffordwolf committed May 28, 2017
    Copy the full SHA
    9ed4c9d View commit details

  2. Add "setundef -anyseq"

    @cliffordwolf
    cliffordwolf committed May 28, 2017
    Copy the full SHA
    05df3db View commit details
Showing with 122 additions and 27 deletions.
  1. +61 −7 backends/aiger/aiger.cc
  2. +4 −4 backends/smt2/smtio.py
  3. +12 −12 kernel/rtlil.h
  4. +43 −3 passes/cmds/setundef.cc
  5. +2 −1 passes/sat/freduce.cc
68 changes: 61 additions & 7 deletions backends/aiger/aiger.cc
View file
Original file line number Diff line number Diff line change
@@ -88,6 +88,9 @@ struct AigerWriter
int a1 = bit2aig(args.second);
aig_map[bit] = mkgate(a0, a1);
}

if (bit == State::Sx || bit == State::Sz)
log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
}

log_assert(aig_map.at(bit) >= 0);
@@ -96,6 +99,9 @@ struct AigerWriter

AigerWriter(Module *module, bool zinit_mode) : module(module), zinit_mode(zinit_mode), sigmap(module)
{
pool<SigBit> undriven_bits;
pool<SigBit> unused_bits;

for (auto wire : module->wires())
{
if (wire->attributes.count("\\init")) {
@@ -106,21 +112,36 @@ struct AigerWriter
init_map[initsig[i]] = initval[i] == State::S1;
}

if (wire->port_input)
for (auto bit : sigmap(wire))
for (auto bit : sigmap(wire))
{
if (bit.wire == nullptr)
continue;

undriven_bits.insert(bit);
unused_bits.insert(bit);

if (wire->port_input)
input_bits.insert(bit);

if (wire->port_output)
for (auto bit : sigmap(wire))
if (wire->port_output)
output_bits.insert(bit);
}
}

for (auto bit : input_bits)
undriven_bits.erase(bit);

for (auto bit : output_bits)
unused_bits.erase(bit);

for (auto cell : module->cells())
{
if (cell->type == "$_NOT_")
{
SigBit A = sigmap(cell->getPort("\\A").as_bit());
SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
unused_bits.erase(A);
undriven_bits.erase(Y);
not_map[Y] = A;
continue;
}
@@ -129,6 +150,8 @@ struct AigerWriter
{
SigBit D = sigmap(cell->getPort("\\D").as_bit());
SigBit Q = sigmap(cell->getPort("\\Q").as_bit());
unused_bits.erase(D);
undriven_bits.erase(Q);
ff_map[Q] = D;
continue;
}
@@ -138,13 +161,17 @@ struct AigerWriter
SigBit A = sigmap(cell->getPort("\\A").as_bit());
SigBit B = sigmap(cell->getPort("\\B").as_bit());
SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
unused_bits.erase(A);
unused_bits.erase(B);
undriven_bits.erase(Y);
and_map[Y] = make_pair(A, B);
continue;
}

if (cell->type == "$initstate")
{
SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
undriven_bits.erase(Y);
initstate_bits.insert(Y);
continue;
}
@@ -153,6 +180,8 @@ struct AigerWriter
{
SigBit A = sigmap(cell->getPort("\\A").as_bit());
SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
unused_bits.erase(A);
unused_bits.erase(EN);
asserts.push_back(make_pair(A, EN));
continue;
}
@@ -161,6 +190,8 @@ struct AigerWriter
{
SigBit A = sigmap(cell->getPort("\\A").as_bit());
SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
unused_bits.erase(A);
unused_bits.erase(EN);
assumes.push_back(make_pair(A, EN));
continue;
}
@@ -169,6 +200,8 @@ struct AigerWriter
{
SigBit A = sigmap(cell->getPort("\\A").as_bit());
SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
unused_bits.erase(A);
unused_bits.erase(EN);
liveness.push_back(make_pair(A, EN));
continue;
}
@@ -177,27 +210,45 @@ struct AigerWriter
{
SigBit A = sigmap(cell->getPort("\\A").as_bit());
SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
unused_bits.erase(A);
unused_bits.erase(EN);
fairness.push_back(make_pair(A, EN));
continue;
}

if (cell->type == "$anyconst")
{
for (auto bit : sigmap(cell->getPort("\\Y")))
for (auto bit : sigmap(cell->getPort("\\Y"))) {
undriven_bits.erase(bit);
ff_map[bit] = bit;
}
continue;
}

if (cell->type == "$anyseq")
{
for (auto bit : sigmap(cell->getPort("\\Y")))
for (auto bit : sigmap(cell->getPort("\\Y"))) {
undriven_bits.erase(bit);
input_bits.insert(bit);
}
continue;
}

log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
}

for (auto bit : unused_bits)
undriven_bits.erase(bit);

if (!undriven_bits.empty()) {
undriven_bits.sort();
for (auto bit : undriven_bits) {
log_warning("Treating undriven bit %s.%s like $anyseq.\n", log_id(module), log_signal(bit));
input_bits.insert(bit);
}
log_warning("Treating a total of %d undriven bits in %s like $anyseq.\n", GetSize(undriven_bits), log_id(module));
}

init_map.sort();
input_bits.sort();
output_bits.sort();
@@ -442,6 +493,9 @@ struct AigerWriter

for (int i = 0; i < GetSize(wire); i++)
{
if (sig[i].wire == nullptr)
continue;

if (wire->port_input) {
int a = aig_map.at(sig[i]);
log_assert((a & 1) == 0);
@@ -500,7 +554,7 @@ struct AigerWriter

for (int i = 0; i < GetSize(wire); i++)
{
if (aig_map.count(sig[i]) == 0)
if (aig_map.count(sig[i]) == 0 || sig[i].wire == nullptr)
continue;

int a = aig_map.at(sig[i]);
8 changes: 4 additions & 4 deletions backends/smt2/smtio.py
View file
Original file line number Diff line number Diff line change
@@ -72,7 +72,7 @@ def __init__(self, opts=None):
self.nocomments = opts.nocomments

else:
self.solver = "z3"
self.solver = "yices"
self.solver_opts = list()
self.debug_print = False
self.debug_file = None
@@ -649,7 +649,7 @@ class SmtOpts:
def __init__(self):
self.shortopts = "s:S:v"
self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.solver = "z3"
self.solver = "yices"
self.solver_opts = list()
self.debug_print = False
self.debug_file = None
@@ -691,8 +691,8 @@ def handle(self, o, a):
def helpmsg(self):
return """
-s <solver>
set SMT solver: z3, cvc4, yices, mathsat, boolector, dummy
default: z3
set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
default: yices
-S <opt>
pass <opt> as command line argument to the solver
24 changes: 12 additions & 12 deletions kernel/rtlil.h
View file
Original file line number Diff line number Diff line change
@@ -911,7 +911,7 @@ struct RTLIL::Module : public RTLIL::AttrObject
std::vector<RTLIL::IdString> ports;
void fixup_ports();

template<typename T> void rewrite_sigspecs(T functor);
template<typename T> void rewrite_sigspecs(T &functor);
void cloneInto(RTLIL::Module *new_mod) const;
virtual RTLIL::Module *clone() const;

@@ -1201,7 +1201,7 @@ struct RTLIL::Cell : public RTLIL::AttrObject
module->design->module(type)->get_bool_attribute("\\keep"));
}

template<typename T> void rewrite_sigspecs(T functor);
template<typename T> void rewrite_sigspecs(T &functor);
};

struct RTLIL::CaseRule
@@ -1213,7 +1213,7 @@ struct RTLIL::CaseRule
~CaseRule();
void optimize();

template<typename T> void rewrite_sigspecs(T functor);
template<typename T> void rewrite_sigspecs(T &functor);
RTLIL::CaseRule *clone() const;
};

@@ -1224,7 +1224,7 @@ struct RTLIL::SwitchRule : public RTLIL::AttrObject

~SwitchRule();

template<typename T> void rewrite_sigspecs(T functor);
template<typename T> void rewrite_sigspecs(T &functor);
RTLIL::SwitchRule *clone() const;
};

@@ -1234,7 +1234,7 @@ struct RTLIL::SyncRule
RTLIL::SigSpec signal;
std::vector<RTLIL::SigSig> actions;

template<typename T> void rewrite_sigspecs(T functor);
template<typename T> void rewrite_sigspecs(T &functor);
RTLIL::SyncRule *clone() const;
};

@@ -1246,7 +1246,7 @@ struct RTLIL::Process : public RTLIL::AttrObject

~Process();

template<typename T> void rewrite_sigspecs(T functor);
template<typename T> void rewrite_sigspecs(T &functor);
RTLIL::Process *clone() const;
};

@@ -1295,7 +1295,7 @@ inline RTLIL::SigBit::SigBit(const RTLIL::SigSpec &sig) {
}

template<typename T>
void RTLIL::Module::rewrite_sigspecs(T functor)
void RTLIL::Module::rewrite_sigspecs(T &functor)
{
for (auto &it : cells_)
it.second->rewrite_sigspecs(functor);
@@ -1308,13 +1308,13 @@ void RTLIL::Module::rewrite_sigspecs(T functor)
}

template<typename T>
void RTLIL::Cell::rewrite_sigspecs(T functor) {
void RTLIL::Cell::rewrite_sigspecs(T &functor) {
for (auto &it : connections_)
functor(it.second);
}

template<typename T>
void RTLIL::CaseRule::rewrite_sigspecs(T functor) {
void RTLIL::CaseRule::rewrite_sigspecs(T &functor) {
for (auto &it : compare)
functor(it);
for (auto &it : actions) {
@@ -1326,15 +1326,15 @@ void RTLIL::CaseRule::rewrite_sigspecs(T functor) {
}

template<typename T>
void RTLIL::SwitchRule::rewrite_sigspecs(T functor)
void RTLIL::SwitchRule::rewrite_sigspecs(T &functor)
{
functor(signal);
for (auto it : cases)
it->rewrite_sigspecs(functor);
}

template<typename T>
void RTLIL::SyncRule::rewrite_sigspecs(T functor)
void RTLIL::SyncRule::rewrite_sigspecs(T &functor)
{
functor(signal);
for (auto &it : actions) {
@@ -1344,7 +1344,7 @@ void RTLIL::SyncRule::rewrite_sigspecs(T functor)
}

template<typename T>
void RTLIL::Process::rewrite_sigspecs(T functor)
void RTLIL::Process::rewrite_sigspecs(T &functor)
{
root_case.rewrite_sigspecs(functor);
for (auto it : syncs)
Loading