PerformReduction Struct Reference

Collaboration diagram for PerformReduction:

Public Member Functions
int	register_cone_worker (std::set< RTLIL::Cell * > &celldone, std::map< RTLIL::SigBit, int > &sigdepth, RTLIL::SigBit out)
	PerformReduction (SigMap &sigmap, drivers_t &drivers, std::set< std::pair< RTLIL::SigBit, RTLIL::SigBit >> &inv_pairs, std::vector< RTLIL::SigBit > &bits, int cone_size)
void	analyze_const (std::vector< std::vector< equiv_bit_t >> &results, int idx)
void	analyze (std::vector< std::set< int >> &results, std::map< int, int > &results_map, std::vector< int > &bucket, std::string indent1, std::string indent2)
void	analyze (std::vector< std::vector< equiv_bit_t >> &results, int perc)

Data Fields
SigMap &	sigmap
drivers_t &	drivers
std::set< std::pair < RTLIL::SigBit, RTLIL::SigBit > > &	inv_pairs
ezDefaultSAT	ez
SatGen	satgen
std::vector< int >	sat_pi
std::vector< int >	sat_out
std::vector< int >	sat_def
std::vector< RTLIL::SigBit >	out_bits
std::vector< RTLIL::SigBit >	pi_bits
std::vector< bool >	out_inverted
std::vector< int >	out_depth
int	cone_size

Detailed Description

Definition at line 227 of file freduce.cc.

Constructor & Destructor Documentation

PerformReduction::PerformReduction ( SigMap &  sigmap, drivers_t &  drivers, std::set< std::pair< RTLIL::SigBit, RTLIL::SigBit >> &  inv_pairs, std::vector< RTLIL::SigBit > &  bits, int  cone_size  )

inline

Definition at line 270 of file freduce.cc.

                                                                                                                                                            :
            sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits), cone_size(cone_size)
    {
        satgen.model_undef = true;

        std::set<RTLIL::Cell*> celldone;
        std::map<RTLIL::SigBit, int> sigdepth;

        for (auto &bit : bits) {
            out_depth.push_back(register_cone_worker(celldone, sigdepth, bit));
            sat_out.push_back(satgen.importSigSpec(bit).front());
            sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front()));
        }

        if (inv_mode && cone_size > 0) {
            if (!ez.solve(sat_out, out_inverted, ez.expression(ezSAT::OpAnd, sat_def)))
                log_error("Solving for initial model failed!\n");
            for (size_t i = 0; i < sat_out.size(); i++)
                if (out_inverted.at(i))
                    sat_out[i] = ez.NOT(sat_out[i]);
        } else
            out_inverted = std::vector<bool>(sat_out.size(), false);
    }

Here is the call graph for this function:

Member Function Documentation

void PerformReduction::analyze ( std::vector< std::set< int >> &  results, std::map< int, int > &  results_map, std::vector< int > &  bucket, std::string  indent1, std::string  indent2  )

inline

Definition at line 338 of file freduce.cc.

    {
        std::string indent = indent1 + indent2;
        const char *indt = indent.c_str();

        if (bucket.size() <= 1)
            return;

        if (verbose_level == 1)
            log("%s  Trying to shatter bucket with %d signals.\n", indt, int(bucket.size()));

        if (verbose_level > 1) {
            std::vector<RTLIL::SigBit> bucket_sigbits;
            for (int idx : bucket)
                bucket_sigbits.push_back(out_bits[idx]);
            log("%s  Trying to shatter bucket with %d signals: %s\n", indt, int(bucket.size()), log_signal(bucket_sigbits));
        }

        std::vector<int> sat_set_list, sat_clr_list;
        for (int idx : bucket) {
            sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
            sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
        }

        std::vector<int> modelVars = sat_out;
        std::vector<bool> model;

        modelVars.insert(modelVars.end(), sat_def.begin(), sat_def.end());
        if (verbose_level >= 2)
            modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end());

        if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list)))
        {
            int iter_count = 1;

            while (1)
            {
                sat_set_list.clear();
                sat_clr_list.clear();

                std::vector<int> sat_def_list;

                for (int idx : bucket)
                    if (!model[sat_out.size() + idx]) {
                        sat_set_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
                        sat_clr_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
                    } else {
                        sat_def_list.push_back(sat_def[idx]);
                    }

                if (!ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_set_list), ez.expression(ezSAT::OpOr, sat_clr_list), ez.expression(ezSAT::OpAnd, sat_def_list)))
                    break;
                iter_count++;
            }

            if (verbose_level >= 1) {
                int count_set = 0, count_clr = 0, count_undef = 0;
                for (int idx : bucket)
                    if (!model[sat_out.size() + idx])
                        count_undef++;
                    else if (model[idx])
                        count_set++;
                    else
                        count_clr++;
                log("%s    After %d iterations: %d set vs. %d clr vs %d undef\n", indt, iter_count, count_set, count_clr, count_undef);
            }

            if (verbose_level >= 2) {
                for (size_t i = 0; i < pi_bits.size(); i++)
                    log("%s       -> PI  %c == %s\n", indt, model[2*sat_out.size() + i] ? '1' : '0', log_signal(pi_bits[i]));
                for (int idx : bucket)
                    log("%s       -> OUT %c == %s%s\n", indt, model[sat_out.size() + idx] ? model[idx] ? '1' : '0' : 'x',
                            out_inverted.at(idx) ? "~" : "", log_signal(out_bits[idx]));
            }

            std::vector<int> buckets_a;
            std::vector<int> buckets_b;

            for (int idx : bucket) {
                if (!model[sat_out.size() + idx] || model[idx])
                    buckets_a.push_back(idx);
                if (!model[sat_out.size() + idx] || !model[idx])
                    buckets_b.push_back(idx);
            }
            analyze(results, results_map, buckets_a, indent1 + ".", indent2 + "  ");
            analyze(results, results_map, buckets_b, indent1 + "x", indent2 + "  ");
        }
        else
        {
            std::vector<int> undef_slaves;

            for (int idx : bucket) {
                std::vector<int> sat_def_list;
                for (int idx2 : bucket)
                    if (idx != idx2)
                        sat_def_list.push_back(sat_def[idx2]);
                if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list)))
                    undef_slaves.push_back(idx);
            }

            if (undef_slaves.size() == bucket.size()) {
                if (verbose_level >= 1)
                    log("%s    Complex undef overlap. None of the signals covers the others.\n", indt);
                // FIXME: We could try to further shatter a group with complex undef overlaps
                return;
            }

            for (int idx : undef_slaves)
                out_depth[idx] = std::numeric_limits<int>::max();

            if (verbose_level >= 1) {
                log("%s    Found %d equivialent signals:", indt, int(bucket.size()));
                for (int idx : bucket)
                    log("%s%s%s", idx == bucket.front() ? " " : ", ", out_inverted[idx] ? "~" : "", log_signal(out_bits[idx]));
                log("\n");
            }

            int result_idx = -1;
            for (int idx : bucket) {
                if (results_map.count(idx) == 0)
                    continue;
                if (result_idx == -1) {
                    result_idx = results_map.at(idx);
                    continue;
                }
                int result_idx2 = results_map.at(idx);
                results[result_idx].insert(results[result_idx2].begin(), results[result_idx2].end());
                for (int idx2 : results[result_idx2])
                    results_map[idx2] = result_idx;
                results[result_idx2].clear();
            }

            if (result_idx == -1) {
                result_idx = results.size();
                results.push_back(std::set<int>());
            }

            results[result_idx].insert(bucket.begin(), bucket.end());
        }
    }

Here is the call graph for this function:

Here is the caller graph for this function:

void PerformReduction::analyze ( std::vector< std::vector< equiv_bit_t >> &  results, int  perc  )

inline

Definition at line 479 of file freduce.cc.

    {
        std::vector<int> bucket;
        for (size_t i = 0; i < sat_out.size(); i++)
            bucket.push_back(i);

        std::vector<std::set<int>> results_buf;
        std::map<int, int> results_map;
        analyze(results_buf, results_map, bucket, stringf("[%2d%%] %d ", perc, cone_size), "");

        for (auto &r : results_buf)
        {
            if (r.size() <= 1)
                continue;

            if (verbose_level >= 1) {
                std::vector<RTLIL::SigBit> r_sigbits;
                for (int idx : r)
                    r_sigbits.push_back(out_bits[idx]);
                log("  Found group of %d equivialent signals: %s\n", int(r.size()), log_signal(r_sigbits));
            }

            std::vector<int> undef_slaves;

            for (int idx : r) {
                std::vector<int> sat_def_list;
                for (int idx2 : r)
                    if (idx != idx2)
                        sat_def_list.push_back(sat_def[idx2]);
                if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list)))
                    undef_slaves.push_back(idx);
            }

            if (undef_slaves.size() == bucket.size()) {
                if (verbose_level >= 1)
                    log("    Complex undef overlap. None of the signals covers the others.\n");
                // FIXME: We could try to further shatter a group with complex undef overlaps
                return;
            }

            for (int idx : undef_slaves)
                out_depth[idx] = std::numeric_limits<int>::max();

            std::vector<equiv_bit_t> result;

            for (int idx : r) {
                equiv_bit_t bit;
                bit.depth = out_depth[idx];
                bit.inverted = out_inverted[idx];
                bit.drv = drivers.count(out_bits[idx]) ? drivers.at(out_bits[idx]).first : NULL;
                bit.bit = out_bits[idx];
                result.push_back(bit);
            }

            std::sort(result.begin(), result.end());

            if (result.front().inverted)
                for (auto &bit : result)
                    bit.inverted = !bit.inverted;

            for (size_t i = 1; i < result.size(); i++) {
                std::pair<RTLIL::SigBit, RTLIL::SigBit> p(result[0].bit, result[i].bit);
                if (inv_pairs.count(p) != 0)
                    result.erase(result.begin() + i);
            }

            if (result.size() > 1)
                results.push_back(result);
        }
    }

Here is the call graph for this function:

void PerformReduction::analyze_const ( std::vector< std::vector< equiv_bit_t >> &  results, int  idx  )

inline

Definition at line 294 of file freduce.cc.

    {
        if (verbose_level == 1)
            log("    Finding const value for %s.\n", log_signal(out_bits[idx]));

        bool can_be_set = ez.solve(ez.AND(sat_out[idx], sat_def[idx]));
        bool can_be_clr = ez.solve(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
        log_assert(!can_be_set || !can_be_clr);

        RTLIL::SigBit value(RTLIL::State::Sx);
        if (can_be_set)
            value = RTLIL::State::S1;
        if (can_be_clr)
            value = RTLIL::State::S0;
        if (verbose_level == 1)
            log("      Constant value for this signal: %s\n", log_signal(value));

        int result_idx = -1;
        for (size_t i = 0; i < results.size(); i++) {
            if (results[i].front().bit == value) {
                result_idx = i;
                break;
            }
        }

        if (result_idx == -1) {
            result_idx = results.size();
            results.push_back(std::vector<equiv_bit_t>());
            equiv_bit_t bit;
            bit.depth = 0;
            bit.inverted = false;
            bit.drv = NULL;
            bit.bit = value;
            results.back().push_back(bit);
        }

        equiv_bit_t bit;
        bit.depth = 1;
        bit.inverted = false;
        bit.drv = drivers.count(out_bits[idx]) ? drivers.at(out_bits[idx]).first : NULL;
        bit.bit = out_bits[idx];
        results[result_idx].push_back(bit);
    }

Here is the call graph for this function:

Here is the caller graph for this function:

int PerformReduction::register_cone_worker ( std::set< RTLIL::Cell * > &  celldone, std::map< RTLIL::SigBit, int > &  sigdepth, RTLIL::SigBit  out  )

inline

Definition at line 242 of file freduce.cc.

    {
        if (out.wire == NULL)
            return 0;
        if (sigdepth.count(out) != 0)
            return sigdepth.at(out);

        if (drivers.count(out) != 0) {
            std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
            if (celldone.count(drv.first) == 0) {
                if (!satgen.importCell(drv.first))
                    log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
                celldone.insert(drv.first);
            }
            int max_child_depth = 0;
            for (auto &bit : drv.second)
                max_child_depth = std::max(register_cone_worker(celldone, sigdepth, bit), max_child_depth);
            sigdepth[out] = max_child_depth + 1;
        } else {
            pi_bits.push_back(out);
            sat_pi.push_back(satgen.importSigSpec(out).front());
            ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front()));
            sigdepth[out] = 0;
        }

        return sigdepth.at(out);
    }

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

int PerformReduction::cone_size

Definition at line 240 of file freduce.cc.

drivers_t& PerformReduction::drivers

Definition at line 230 of file freduce.cc.

ezDefaultSAT PerformReduction::ez

Definition at line 233 of file freduce.cc.

std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit> >& PerformReduction::inv_pairs

Definition at line 231 of file freduce.cc.

std::vector<RTLIL::SigBit> PerformReduction::out_bits

Definition at line 237 of file freduce.cc.

std::vector<int> PerformReduction::out_depth

Definition at line 239 of file freduce.cc.

std::vector<bool> PerformReduction::out_inverted

Definition at line 238 of file freduce.cc.

std::vector<RTLIL::SigBit> PerformReduction::pi_bits

Definition at line 237 of file freduce.cc.

std::vector<int> PerformReduction::sat_def

Definition at line 236 of file freduce.cc.

std::vector<int> PerformReduction::sat_out

Definition at line 236 of file freduce.cc.

std::vector<int> PerformReduction::sat_pi

Definition at line 236 of file freduce.cc.

SatGen PerformReduction::satgen

Definition at line 234 of file freduce.cc.

SigMap& PerformReduction::sigmap

Definition at line 229 of file freduce.cc.

---

The documentation for this struct was generated from the following file:

• freduce.cc