Collaboration diagram for SatHelper:

Data Structures
struct	ModelBlockInfo

Public Member Functions
	SatHelper (RTLIL::Design design, RTLIL::Module module, bool enable_undef)

void	check_undef_enabled (const RTLIL::SigSpec &sig)

void	setup_init ()

void	setup (int timestep=-1)

int	setup_proof (int timestep=-1)

void	force_unique_state (int timestep_from, int timestep_to)

bool	solve (const std::vector< int > &assumptions)

bool	solve (int a=0, int b=0, int c=0, int d=0, int e=0, int f=0)

void	maximize_undefs ()

void	generate_model ()

void	print_model ()

void	dump_model_to_vcd (std::string vcd_file_name)

void	invalidate_model (bool max_undef)

Data Fields
RTLIL::Design *	design

RTLIL::Module *	module

ezDefaultSAT	ez

SigMap	sigmap

CellTypes	ct

SatGen	satgen

std::vector< std::pair < std::string, std::string > >	sets

std::vector< std::pair < std::string, std::string > >	prove

std::vector< std::pair < std::string, std::string > >	prove_x

std::vector< std::pair < std::string, std::string > >	sets_init

std::map< int, std::vector < std::pair< std::string, std::string > > >	sets_at

std::map< int, std::vector < std::string > >	unsets_at

bool	prove_asserts

bool	enable_undef

bool	set_init_def

bool	set_init_undef

bool	set_init_zero

bool	ignore_unknown_cells

std::vector< std::string >	sets_def

std::vector< std::string >	sets_any_undef

std::vector< std::string >	sets_all_undef

std::map< int, std::vector < std::string > >	sets_def_at

std::map< int, std::vector < std::string > >	sets_any_undef_at

std::map< int, std::vector < std::string > >	sets_all_undef_at

std::vector< std::string >	shows

SigPool	show_signal_pool

SigSet< RTLIL::Cell * >	show_drivers

int	max_timestep

int	timeout

bool	gotTimeout

std::vector< int >	modelExpressions

std::vector< bool >	modelValues

std::set< ModelBlockInfo >	modelInfo

Detailed Description

Definition at line 39 of file sat.cc.

Constructor & Destructor Documentation

SatHelper::SatHelper	(	RTLIL::Design *	design,
		RTLIL::Module *	module,
		bool	enable_undef
	)

inline

Definition at line 67 of file sat.cc.

                                                                            :
         design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap)
     {
         this->enable_undef = enable_undef;
         satgen.model_undef = enable_undef;
         set_init_def = false;
         set_init_undef = false;
         set_init_zero = false;
         ignore_unknown_cells = false;
         max_timestep = -1;
         timeout = 0;
         gotTimeout = false;
     }

Member Function Documentation

void SatHelper::check_undef_enabled ( const RTLIL::SigSpec & sig )

inline

Definition at line 81 of file sat.cc.

     {
         if (enable_undef)
             return;
 
         std::vector<RTLIL::SigBit> sigbits = sig.to_sigbit_vector();
         for (size_t i = 0; i < sigbits.size(); i++)
             if (sigbits[i].wire == NULL && sigbits[i].data == RTLIL::State::Sx)
                 log_cmd_error("Bit %d of %s is undef but option -enable_undef is missing!\n", int(i), log_signal(sig));
     }

Here is the call graph for this function:

Here is the caller graph for this function:

void SatHelper::dump_model_to_vcd ( std::string vcd_file_name )

inline

Definition at line 650 of file sat.cc.

     {
         FILE *f = fopen(vcd_file_name.c_str(), "w");
         if (!f)
             log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno));
 
         log("Dumping SAT model to VCD file %s\n", vcd_file_name.c_str());
 
         time_t timestamp;
         struct tm* now;
         char stime[128] = {};
         time(&timestamp);
         now = localtime(&timestamp);
         strftime(stime, sizeof(stime), "%c", now);
 
         std::string module_fname = "unknown";
         auto apos = module->attributes.find("\\src");
         if(apos != module->attributes.end())
             module_fname = module->attributes["\\src"].decode_string();
 
         fprintf(f, "$date\n");
         fprintf(f, "    %s\n", stime);
         fprintf(f, "$end\n");
         fprintf(f, "$version\n");
         fprintf(f, "    Generated by %s\n", yosys_version_str); 
         fprintf(f, "$end\n");
         fprintf(f, "$comment\n");
         fprintf(f, "    Generated from SAT problem in module %s (declared at %s)\n",
             module->name.c_str(), module_fname.c_str());
         fprintf(f, "$end\n");
 
         // VCD has some limits on internal (non-display) identifier names, so make legal ones
         std::map<std::string, std::string> vcdnames;
 
         fprintf(f, "$timescale 1ns\n"); // arbitrary time scale since actual clock period is unknown/unimportant
         fprintf(f, "$scope module %s $end\n", module->name.c_str());
         for (auto &info : modelInfo)
         {
             if (vcdnames.find(info.description) != vcdnames.end())
                 continue;
 
             char namebuf[16];
             snprintf(namebuf, sizeof(namebuf), "v%d", static_cast<int>(vcdnames.size()));
             vcdnames[info.description] = namebuf;
 
             // Even display identifiers can't use some special characters
             std::string legal_desc = info.description.c_str();
             for (auto &c : legal_desc) {
                 if(c == '$')
                     c = '_';
                 if(c == ':')
                     c = '_';
             }
 
             fprintf(f, "$var wire %d %s %s $end\n", info.width, namebuf, legal_desc.c_str());
 
             // Need to look at first *two* cycles!
             // We need to put a name on all variables but those without an initialization clause
             // have no value at timestep 0
             if(info.timestep > 1)
                 break;
         }
         fprintf(f, "$upscope $end\n");
         fprintf(f, "$enddefinitions $end\n");
         fprintf(f, "$dumpvars\n");
 
         static const char bitvals[] = "01xzxx";
 
         int last_timestep = -2;
         for (auto &info : modelInfo)
         {
             RTLIL::Const value;
 
             for (int i = 0; i < info.width; i++) {
                 value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
                 if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
                     value.bits.back() = RTLIL::State::Sx;
             }
 
             if (info.timestep != last_timestep) {
                 if(last_timestep == 0)
                     fprintf(f, "$end\n");
                 else
                     fprintf(f, "#%d\n", info.timestep);
                 last_timestep = info.timestep;
             }
 
             if(info.width == 1) {
                 fprintf(f, "%c%s\n", bitvals[value.bits[0]], vcdnames[info.description].c_str());
             } else {
                 fprintf(f, "b");
                 for(int k=info.width-1; k >= 0; k --)   //need to flip bit ordering for VCD
                     fprintf(f, "%c", bitvals[value.bits[k]]);
                 fprintf(f, " %s\n", vcdnames[info.description].c_str());
             }
         }
 
         if (last_timestep == -2)
             log("  no model variables selected for display.\n");
 
         fclose(f);
     }

Here is the call graph for this function:

Here is the caller graph for this function:

void SatHelper::force_unique_state	(	int	timestep_from,
		int	timestep_to
	)

inline

Definition at line 418 of file sat.cc.

     {
         RTLIL::SigSpec state_signals = satgen.initial_state.export_all();
         for (int i = timestep_from; i < timestep_to; i++)
             ez.assume(ez.NOT(satgen.signals_eq(state_signals, state_signals, i, timestep_to)));
     }

Here is the call graph for this function:

Here is the caller graph for this function:

void SatHelper::generate_model ( )

inline

Definition at line 488 of file sat.cc.

     {
         RTLIL::SigSpec modelSig;
         modelExpressions.clear();
         modelInfo.clear();
 
         // Add "show" signals or alternatively the leaves on the input cone on all set and prove signals
 
         if (shows.size() == 0)
         {
             SigPool queued_signals, handled_signals, final_signals;
             queued_signals = show_signal_pool;
             while (queued_signals.size() > 0) {
                 RTLIL::SigSpec sig = queued_signals.export_one();
                 queued_signals.del(sig);
                 handled_signals.add(sig);
                 std::set<RTLIL::Cell*> drivers = show_drivers.find(sig);
                 if (drivers.size() == 0) {
                     final_signals.add(sig);
                 } else {
                     for (auto &d : drivers)
                     for (auto &p : d->connections()) {
                         if (d->type == "$dff" && p.first == "\\CLK")
                             continue;
                         if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
                             continue;
                         queued_signals.add(handled_signals.remove(sigmap(p.second)));
                     }
                 }
             }
             modelSig = final_signals.export_all();
 
             // additionally add all set and prove signals directly
             // (it improves user confidence if we write the constraints back ;-)
             modelSig.append(show_signal_pool.export_all());
         }
         else
         {
             for (auto &s : shows) {
                 RTLIL::SigSpec sig;
                 if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
                     log_cmd_error("Failed to parse show expression `%s'.\n", s.c_str());
                 log("Import show expression: %s\n", log_signal(sig));
                 modelSig.append(sig);
             }
         }
 
         modelSig.sort_and_unify();
         // log("Model signals: %s\n", log_signal(modelSig));
 
         std::vector<int> modelUndefExpressions;
 
         for (auto &c : modelSig.chunks())
             if (c.wire != NULL)
             {
                 ModelBlockInfo info;
                 RTLIL::SigSpec chunksig = c;
                 info.width = chunksig.size();
                 info.description = log_signal(chunksig);
 
                 for (int timestep = -1; timestep <= max_timestep; timestep++)
                 {
                     if ((timestep == -1 && max_timestep > 0) || timestep == 0)
                         continue;
 
                     info.timestep = timestep;
                     info.offset = modelExpressions.size();
                     modelInfo.insert(info);
 
                     std::vector<int> vec = satgen.importSigSpec(chunksig, timestep);
                     modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
 
                     if (enable_undef) {
                         std::vector<int> undef_vec = satgen.importUndefSigSpec(chunksig, timestep);
                         modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end());
                     }
                 }
             }
 
         // Add initial state signals as collected by satgen
         //
         modelSig = satgen.initial_state.export_all();
         for (auto &c : modelSig.chunks())
             if (c.wire != NULL)
             {
                 ModelBlockInfo info;
                 RTLIL::SigSpec chunksig = c;
 
                 info.timestep = 0;
                 info.offset = modelExpressions.size();
                 info.width = chunksig.size();
                 info.description = log_signal(chunksig);
                 modelInfo.insert(info);
 
                 std::vector<int> vec = satgen.importSigSpec(chunksig, 1);
                 modelExpressions.insert(modelExpressions.end(), vec.begin(), vec.end());
 
                 if (enable_undef) {
                     std::vector<int> undef_vec = satgen.importUndefSigSpec(chunksig, 1);
                     modelUndefExpressions.insert(modelUndefExpressions.end(), undef_vec.begin(), undef_vec.end());
                 }
             }
 
         modelExpressions.insert(modelExpressions.end(), modelUndefExpressions.begin(), modelUndefExpressions.end());
     }

Here is the call graph for this function:

Here is the caller graph for this function:

void SatHelper::invalidate_model ( bool max_undef )

inline

Definition at line 753 of file sat.cc.

     {
         std::vector<int> clause;
         if (enable_undef) {
             for (size_t i = 0; i < modelExpressions.size()/2; i++) {
                 int bit = modelExpressions.at(i), bit_undef = modelExpressions.at(modelExpressions.size()/2 + i);
                 bool val = modelValues.at(i), val_undef = modelValues.at(modelExpressions.size()/2 + i);
                 if (!max_undef || !val_undef)
                     clause.push_back(val_undef ? ez.NOT(bit_undef) : val ? ez.NOT(bit) : bit);
             }
         } else
             for (size_t i = 0; i < modelExpressions.size(); i++)
                 clause.push_back(modelValues.at(i) ? ez.NOT(modelExpressions.at(i)) : modelExpressions.at(i));
         ez.assume(ez.expression(ezSAT::OpOr, clause));
     }

Here is the caller graph for this function:

void SatHelper::maximize_undefs ( )

inline

Definition at line 465 of file sat.cc.

     {
         log_assert(enable_undef);
         std::vector<bool> backupValues;
 
         while (1)
         {
             std::vector<int> must_undef, maybe_undef;
 
             for (size_t i = 0; i < modelExpressions.size()/2; i++)
                 if (modelValues.at(modelExpressions.size()/2 + i))
                     must_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
                 else
                     maybe_undef.push_back(modelExpressions.at(modelExpressions.size()/2 + i));
 
             backupValues.swap(modelValues);
             if (!solve(ez.expression(ezSAT::OpAnd, must_undef), ez.expression(ezSAT::OpOr, maybe_undef)))
                 break;
         }
 
         backupValues.swap(modelValues);
     }

Here is the call graph for this function:

Here is the caller graph for this function:

void SatHelper::print_model ( )

inline

Definition at line 594 of file sat.cc.

     {
         int maxModelName = 10;
         int maxModelWidth = 10;
 
         for (auto &info : modelInfo) {
             maxModelName = std::max(maxModelName, int(info.description.size()));
             maxModelWidth = std::max(maxModelWidth, info.width);
         }
 
         log("\n");
 
         int last_timestep = -2;
         for (auto &info : modelInfo)
         {
             RTLIL::Const value;
             bool found_undef = false;
 
             for (int i = 0; i < info.width; i++) {
                 value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0);
                 if (enable_undef && modelValues.at(modelExpressions.size()/2 + info.offset + i))
                     value.bits.back() = RTLIL::State::Sx, found_undef = true;
             }
 
             if (info.timestep != last_timestep) {
                 const char *hline = "---------------------------------------------------------------------------------------------------"
                             "---------------------------------------------------------------------------------------------------"
                             "---------------------------------------------------------------------------------------------------";
                 if (last_timestep == -2) {
                     log(max_timestep > 0 ? "  Time " : "  ");
                     log("%-*s %10s %10s %*s\n", maxModelName+10, "Signal Name", "Dec", "Hex", maxModelWidth+5, "Bin");
                 }
                 log(max_timestep > 0 ? "  ---- " : "  ");
                 log("%*.*s %10.10s %10.10s %*.*s\n", maxModelName+10, maxModelName+10,
                         hline, hline, hline, maxModelWidth+5, maxModelWidth+5, hline);
                 last_timestep = info.timestep;
             }
 
             if (max_timestep > 0) {
                 if (info.timestep > 0)
                     log("  %4d ", info.timestep);
                 else
                     log("  init ");
             } else
                 log("  ");
 
             if (info.width <= 32 && !found_undef)
                 log("%-*s %10d %10x %*s\n", maxModelName+10, info.description.c_str(), value.as_int(), value.as_int(), maxModelWidth+5, value.as_string().c_str());
             else
                 log("%-*s %10s %10s %*s\n", maxModelName+10, info.description.c_str(), "--", "--", maxModelWidth+5, value.as_string().c_str());
         }
 
         if (last_timestep == -2)
             log("  no model variables selected for display.\n");
     }

Here is the call graph for this function:

Here is the caller graph for this function:

void SatHelper::setup ( int timestep = -1 )

inline

Definition at line 185 of file sat.cc.

     {
         if (timestep > 0)
             log ("\nSetting up time step %d:\n", timestep);
         else
             log ("\nSetting up SAT problem:\n");
 
         if (timestep > max_timestep)
             max_timestep = timestep;
 
         RTLIL::SigSpec big_lhs, big_rhs;
 
         for (auto &s : sets)
         {
             RTLIL::SigSpec lhs, rhs;
 
             if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
             if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
                 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
             show_signal_pool.add(sigmap(lhs));
             show_signal_pool.add(sigmap(rhs));
 
             if (lhs.size() != rhs.size())
                 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
                     s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
             log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
             big_lhs.remove2(lhs, &big_rhs);
             big_lhs.append(lhs);
             big_rhs.append(rhs);
         }
 
         for (auto &s : sets_at[timestep])
         {
             RTLIL::SigSpec lhs, rhs;
 
             if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
             if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
                 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
             show_signal_pool.add(sigmap(lhs));
             show_signal_pool.add(sigmap(rhs));
 
             if (lhs.size() != rhs.size())
                 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
                     s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
             log("Import set-constraint for this timestep: %s = %s\n", log_signal(lhs), log_signal(rhs));
             big_lhs.remove2(lhs, &big_rhs);
             big_lhs.append(lhs);
             big_rhs.append(rhs);
         }
 
         for (auto &s : unsets_at[timestep])
         {
             RTLIL::SigSpec lhs;
 
             if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s))
                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.c_str());
             show_signal_pool.add(sigmap(lhs));
 
             log("Import unset-constraint for this timestep: %s\n", log_signal(lhs));
             big_lhs.remove2(lhs, &big_rhs);
         }
 
         log("Final constraint equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
         check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
         ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
 
         // 0 = sets_def
         // 1 = sets_any_undef
         // 2 = sets_all_undef
         std::set<RTLIL::SigSpec> sets_def_undef[3];
 
         for (auto &s : sets_def) {
             RTLIL::SigSpec sig;
             if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
                 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
             sets_def_undef[0].insert(sig);
         }
 
         for (auto &s : sets_any_undef) {
             RTLIL::SigSpec sig;
             if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
                 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
             sets_def_undef[1].insert(sig);
         }
 
         for (auto &s : sets_all_undef) {
             RTLIL::SigSpec sig;
             if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
                 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
             sets_def_undef[2].insert(sig);
         }
 
         for (auto &s : sets_def_at[timestep]) {
             RTLIL::SigSpec sig;
             if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
                 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
             sets_def_undef[0].insert(sig);
             sets_def_undef[1].erase(sig);
             sets_def_undef[2].erase(sig);
         }
 
         for (auto &s : sets_any_undef_at[timestep]) {
             RTLIL::SigSpec sig;
             if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
                 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
             sets_def_undef[0].erase(sig);
             sets_def_undef[1].insert(sig);
             sets_def_undef[2].erase(sig);
         }
 
         for (auto &s : sets_all_undef_at[timestep]) {
             RTLIL::SigSpec sig;
             if (!RTLIL::SigSpec::parse_sel(sig, design, module, s))
                 log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
             sets_def_undef[0].erase(sig);
             sets_def_undef[1].erase(sig);
             sets_def_undef[2].insert(sig);
         }
 
         for (int t = 0; t < 3; t++)
         for (auto &sig : sets_def_undef[t]) {
             log("Import %s constraint for this timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
             std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
             if (t == 0)
                 ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
             if (t == 1)
                 ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
             if (t == 2)
                 ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
         }
 
         int import_cell_counter = 0;
         for (auto &c : module->cells_)
             if (design->selected(module, c.second)) {
                 // log("Import cell: %s\n", RTLIL::id2cstr(c.first));
                 if (satgen.importCell(c.second, timestep)) {
                     for (auto &p : c.second->connections())
                         if (ct.cell_output(c.second->type, p.first))
                             show_drivers.insert(sigmap(p.second), c.second);
                     import_cell_counter++;
                 } else if (ignore_unknown_cells)
                     log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
                 else
                     log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
         }
         log("Imported %d cells to SAT database.\n", import_cell_counter);
     }

Here is the call graph for this function:

Here is the caller graph for this function:

void SatHelper::setup_init ( )

inline

Definition at line 92 of file sat.cc.

     {
         log ("\nSetting up initial state:\n");
 
         RTLIL::SigSpec big_lhs, big_rhs;
 
         for (auto &it : module->wires_)
         {
             if (it.second->attributes.count("\\init") == 0)
                 continue;
 
             RTLIL::SigSpec lhs = sigmap(it.second);
             RTLIL::SigSpec rhs = it.second->attributes.at("\\init");
             log_assert(lhs.size() == rhs.size());
 
             RTLIL::SigSpec removed_bits;
             for (int i = 0; i < lhs.size(); i++) {
                 RTLIL::SigSpec bit = lhs.extract(i, 1);
                 if (!satgen.initial_state.check_all(bit)) {
                     removed_bits.append(bit);
                     lhs.remove(i, 1);
                     rhs.remove(i, 1);
                     i--;
                 }
             }
 
             if (removed_bits.size())
                 log_warning("ignoring initial value on non-register: %s\n", log_signal(removed_bits));
 
             if (lhs.size()) {
                 log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs));
                 big_lhs.remove2(lhs, &big_rhs);
                 big_lhs.append(lhs);
                 big_rhs.append(rhs);
             }
         }
 
         for (auto &s : sets_init)
         {
             RTLIL::SigSpec lhs, rhs;
 
             if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
                 log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
             if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
                 log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
             show_signal_pool.add(sigmap(lhs));
             show_signal_pool.add(sigmap(rhs));
 
             if (lhs.size() != rhs.size())
                 log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
                     s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
             log("Import set-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
             big_lhs.remove2(lhs, &big_rhs);
             big_lhs.append(lhs);
             big_rhs.append(rhs);
         }
 
         if (!satgen.initial_state.check_all(big_lhs)) {
             RTLIL::SigSpec rem = satgen.initial_state.remove(big_lhs);
             log_cmd_error("Found -set-init bits that are not part of the initial_state: %s\n", log_signal(rem));
         }
 
         if (set_init_def) {
             RTLIL::SigSpec rem = satgen.initial_state.export_all();
             std::vector<int> undef_rem = satgen.importUndefSigSpec(rem, 1);
             ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_rem)));
         }
 
         if (set_init_undef) {
             RTLIL::SigSpec rem = satgen.initial_state.export_all();
             rem.remove(big_lhs);
             big_lhs.append(rem);
             big_rhs.append(RTLIL::SigSpec(RTLIL::State::Sx, rem.size()));
         }
 
         if (set_init_zero) {
             RTLIL::SigSpec rem = satgen.initial_state.export_all();
             rem.remove(big_lhs);
             big_lhs.append(rem);
             big_rhs.append(RTLIL::SigSpec(RTLIL::State::S0, rem.size()));
         }
 
         if (big_lhs.size() == 0) {
             log("No constraints for initial state found.\n\n");
             return;
         }
 
         log("Final constraint equation: %s = %s\n\n", log_signal(big_lhs), log_signal(big_rhs));
         check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
         ez.assume(satgen.signals_eq(big_lhs, big_rhs, 1));
     }

Here is the call graph for this function:

Here is the caller graph for this function:

int SatHelper::setup_proof ( int timestep = -1 )

inline

Definition at line 337 of file sat.cc.

     {
         log_assert(prove.size() || prove_x.size() || prove_asserts);
 
         RTLIL::SigSpec big_lhs, big_rhs;
         std::vector<int> prove_bits;
 
         if (prove.size() > 0)
         {
             for (auto &s : prove)
             {
                 RTLIL::SigSpec lhs, rhs;
 
                 if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
                     log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
                 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
                     log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
                 show_signal_pool.add(sigmap(lhs));
                 show_signal_pool.add(sigmap(rhs));
 
                 if (lhs.size() != rhs.size())
                     log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
                         s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
                 log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
                 big_lhs.remove2(lhs, &big_rhs);
                 big_lhs.append(lhs);
                 big_rhs.append(rhs);
             }
 
             log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
             check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
             prove_bits.push_back(satgen.signals_eq(big_lhs, big_rhs, timestep));
         }
 
         if (prove_x.size() > 0)
         {
             for (auto &s : prove_x)
             {
                 RTLIL::SigSpec lhs, rhs;
 
                 if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
                     log_cmd_error("Failed to parse lhs proof-x expression `%s'.\n", s.first.c_str());
                 if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
                     log_cmd_error("Failed to parse rhs proof-x expression `%s'.\n", s.second.c_str());
                 show_signal_pool.add(sigmap(lhs));
                 show_signal_pool.add(sigmap(rhs));
 
                 if (lhs.size() != rhs.size())
                     log_cmd_error("Proof-x expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
                         s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());
 
                 log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
                 big_lhs.remove2(lhs, &big_rhs);
                 big_lhs.append(lhs);
                 big_rhs.append(rhs);
             }
 
             log("Final proof-x equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
 
             std::vector<int> value_lhs = satgen.importDefSigSpec(big_lhs, timestep);
             std::vector<int> value_rhs = satgen.importDefSigSpec(big_rhs, timestep);
 
             std::vector<int> undef_lhs = satgen.importUndefSigSpec(big_lhs, timestep);
             std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
 
             for (size_t i = 0; i < value_lhs.size(); i++)
                 prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
         }
 
         if (prove_asserts) {
             RTLIL::SigSpec asserts_a, asserts_en;
             satgen.getAsserts(asserts_a, asserts_en, timestep);
             for (int i = 0; i < GetSize(asserts_a); i++)
                 log("Import proof for assert: %s when %s.\n", log_signal(asserts_a[i]), log_signal(asserts_en[i]));
             prove_bits.push_back(satgen.importAsserts(timestep));
         }
 
         return ez.expression(ezSAT::OpAnd, prove_bits);
     }

Here is the call graph for this function:

Here is the caller graph for this function:

bool SatHelper::solve ( const std::vector< int > & assumptions )

inline

Definition at line 425 of file sat.cc.

     {
         log_assert(gotTimeout == false);
         ez.setSolverTimeout(timeout);
         bool success = ez.solve(modelExpressions, modelValues, assumptions);
         if (ez.getSolverTimoutStatus())
             gotTimeout = true;
         return success;
     }

Here is the caller graph for this function:

bool SatHelper::solve	(	int	a = `0`,
		int	b = `0`,
		int	c = `0`,
		int	d = `0`,
		int	e = `0`,
		int	f = `0`
	)

inline

Definition at line 435 of file sat.cc.

     {
         log_assert(gotTimeout == false);
         ez.setSolverTimeout(timeout);
         bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f);
         if (ez.getSolverTimoutStatus())
             gotTimeout = true;
         return success;
     }

Field Documentation

CellTypes SatHelper::ct

Definition at line 46 of file sat.cc.

RTLIL::Design* SatHelper::design

Definition at line 41 of file sat.cc.

bool SatHelper::enable_undef

Definition at line 56 of file sat.cc.

ezDefaultSAT SatHelper::ez

Definition at line 44 of file sat.cc.

bool SatHelper::gotTimeout

Definition at line 65 of file sat.cc.

bool SatHelper::ignore_unknown_cells

Definition at line 56 of file sat.cc.

int SatHelper::max_timestep

Definition at line 64 of file sat.cc.

std::vector<int> SatHelper::modelExpressions

Definition at line 461 of file sat.cc.

std::set<ModelBlockInfo> SatHelper::modelInfo

Definition at line 463 of file sat.cc.

std::vector<bool> SatHelper::modelValues

Definition at line 462 of file sat.cc.

RTLIL::Module* SatHelper::module

Definition at line 42 of file sat.cc.

std::vector<std::pair<std::string, std::string> > SatHelper::prove

Definition at line 50 of file sat.cc.

bool SatHelper::prove_asserts

Definition at line 53 of file sat.cc.

std::vector<std::pair<std::string, std::string> > SatHelper::prove_x

Definition at line 50 of file sat.cc.

SatGen SatHelper::satgen

Definition at line 47 of file sat.cc.

bool SatHelper::set_init_def

Definition at line 56 of file sat.cc.

bool SatHelper::set_init_undef

Definition at line 56 of file sat.cc.

bool SatHelper::set_init_zero

Definition at line 56 of file sat.cc.

std::vector<std::pair<std::string, std::string> > SatHelper::sets

Definition at line 50 of file sat.cc.

std::vector<std::string> SatHelper::sets_all_undef

Definition at line 57 of file sat.cc.

std::map<int, std::vector<std::string> > SatHelper::sets_all_undef_at

Definition at line 58 of file sat.cc.

std::vector<std::string> SatHelper::sets_any_undef

Definition at line 57 of file sat.cc.

std::map<int, std::vector<std::string> > SatHelper::sets_any_undef_at

Definition at line 58 of file sat.cc.

std::map<int, std::vector<std::pair<std::string, std::string> > > SatHelper::sets_at

Definition at line 51 of file sat.cc.

std::vector<std::string> SatHelper::sets_def

Definition at line 57 of file sat.cc.

std::map<int, std::vector<std::string> > SatHelper::sets_def_at

Definition at line 58 of file sat.cc.

std::vector<std::pair<std::string, std::string> > SatHelper::sets_init

Definition at line 50 of file sat.cc.

SigSet<RTLIL::Cell*> SatHelper::show_drivers

Definition at line 63 of file sat.cc.

SigPool SatHelper::show_signal_pool

Definition at line 62 of file sat.cc.

std::vector<std::string> SatHelper::shows

Definition at line 61 of file sat.cc.

SigMap SatHelper::sigmap

Definition at line 45 of file sat.cc.

int SatHelper::timeout

Definition at line 64 of file sat.cc.

std::map<int, std::vector<std::string> > SatHelper::unsets_at

Definition at line 52 of file sat.cc.

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

sat.cc

Data Structures

Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation