*
*/
+// [[CITE]] Btor2 , BtorMC and Boolector 3.0
+// Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
+// Computer Aided Verification - 30th International Conference, CAV 2018
+// https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/
+
#include "kernel/rtlil.h"
#include "kernel/register.h"
#include "kernel/sigtools.h"
RTLIL::Module *module;
bool verbose;
bool single_bad;
+ bool cover_mode;
int next_nid = 1;
int initstate_nid = -1;
vector<int> bad_properties;
dict<SigBit, bool> initbits;
pool<Wire*> statewires;
- string indent;
+ pool<string> srcsymbols;
+
+ string indent, info_filename;
+ vector<string> info_lines;
+ dict<int, int> info_clocks;
void btorf(const char *fmt, ...)
{
va_end(ap);
}
+ void infof(const char *fmt, ...)
+ {
+ va_list ap;
+ va_start(ap, fmt);
+ info_lines.push_back(vstringf(fmt, ap));
+ va_end(ap);
+ }
+
+ template<typename T>
+ string getinfo(T *obj, bool srcsym = false)
+ {
+ string infostr = log_id(obj);
+ if (obj->attributes.count("\\src")) {
+ string src = obj->attributes.at("\\src").decode_string().c_str();
+ if (srcsym && infostr[0] == '$') {
+ std::replace(src.begin(), src.end(), ' ', '_');
+ if (srcsymbols.count(src) || module->count_id("\\" + src)) {
+ for (int i = 1;; i++) {
+ string s = stringf("%s-%d", src.c_str(), i);
+ if (!srcsymbols.count(s) && !module->count_id("\\" + s)) {
+ src = s;
+ break;
+ }
+ }
+ }
+ srcsymbols.insert(src);
+ infostr = src;
+ } else {
+ infostr += " ; " + src;
+ }
+ }
+ return infostr;
+ }
+
void btorf_push(const string &id)
{
if (verbose) {
if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor";
log_assert(!btor_op.empty());
- int width = GetSize(cell->getPort("\\Y"));
- width = std::max(width, GetSize(cell->getPort("\\A")));
- width = std::max(width, GetSize(cell->getPort("\\B")));
+ int width = GetSize(cell->getPort(ID::Y));
+ width = std::max(width, GetSize(cell->getPort(ID::A)));
+ width = std::max(width, GetSize(cell->getPort(ID::B)));
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
if (btor_op == "shift")
{
- int nid_a = get_sig_nid(cell->getPort("\\A"), width, false);
- int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+ int nid_a = get_sig_nid(cell->getPort(ID::A), width, false);
+ int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
int nid_r = next_nid++;
btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero);
nid = next_nid++;
- btorf("%d ite %d %d %d %d\n", nid, sid, nid_b_ltz, nid_l, nid_r);
+ btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_b_ltz, nid_l, nid_r, getinfo(cell).c_str());
}
else
{
- int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
- int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+ int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
+ int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
nid = next_nid++;
- btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
+ btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
}
- SigSpec sig = sigmap(cell->getPort("\\Y"));
+ SigSpec sig = sigmap(cell->getPort(ID::Y));
if (GetSize(sig) < width) {
int sid = get_bv_sid(GetSize(sig));
if (cell->type == "$mod") btor_op = "rem";
log_assert(!btor_op.empty());
- int width = GetSize(cell->getPort("\\Y"));
- width = std::max(width, GetSize(cell->getPort("\\A")));
- width = std::max(width, GetSize(cell->getPort("\\B")));
+ int width = GetSize(cell->getPort(ID::Y));
+ width = std::max(width, GetSize(cell->getPort(ID::A)));
+ width = std::max(width, GetSize(cell->getPort(ID::B)));
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
- int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
- int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+ int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
+ int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
int sid = get_bv_sid(width);
int nid = next_nid++;
- btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b);
+ btorf("%d %c%s %d %d %d %s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
- SigSpec sig = sigmap(cell->getPort("\\Y"));
+ SigSpec sig = sigmap(cell->getPort(ID::Y));
if (GetSize(sig) < width) {
int sid = get_bv_sid(GetSize(sig));
if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
{
int sid = get_bv_sid(1);
- int nid_a = get_sig_nid(cell->getPort("\\A"));
- int nid_b = get_sig_nid(cell->getPort("\\B"));
+ int nid_a = get_sig_nid(cell->getPort(ID::A));
+ int nid_b = get_sig_nid(cell->getPort(ID::B));
int nid1 = next_nid++;
int nid2 = next_nid++;
if (cell->type == "$_ANDNOT_") {
btorf("%d not %d %d\n", nid1, sid, nid_b);
- btorf("%d and %d %d %d\n", nid2, sid, nid_a, nid1);
+ btorf("%d and %d %d %d %s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str());
}
if (cell->type == "$_ORNOT_") {
btorf("%d not %d %d\n", nid1, sid, nid_b);
- btorf("%d or %d %d %d\n", nid2, sid, nid_a, nid1);
+ btorf("%d or %d %d %d %s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str());
}
- SigSpec sig = sigmap(cell->getPort("\\Y"));
+ SigSpec sig = sigmap(cell->getPort(ID::Y));
add_nid_sig(nid2, sig);
goto okay;
}
if (cell->type.in("$_OAI3_", "$_AOI3_"))
{
int sid = get_bv_sid(1);
- int nid_a = get_sig_nid(cell->getPort("\\A"));
- int nid_b = get_sig_nid(cell->getPort("\\B"));
+ int nid_a = get_sig_nid(cell->getPort(ID::A));
+ int nid_b = get_sig_nid(cell->getPort(ID::B));
int nid_c = get_sig_nid(cell->getPort("\\C"));
int nid1 = next_nid++;
if (cell->type == "$_OAI3_") {
btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
btorf("%d and %d %d %d\n", nid2, sid, nid1, nid_c);
- btorf("%d not %d %d\n", nid3, sid, nid2);
+ btorf("%d not %d %d %s\n", nid3, sid, nid2, getinfo(cell).c_str());
}
if (cell->type == "$_AOI3_") {
btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
btorf("%d or %d %d %d\n", nid2, sid, nid1, nid_c);
- btorf("%d not %d %d\n", nid3, sid, nid2);
+ btorf("%d not %d %d %s\n", nid3, sid, nid2, getinfo(cell).c_str());
}
- SigSpec sig = sigmap(cell->getPort("\\Y"));
+ SigSpec sig = sigmap(cell->getPort(ID::Y));
add_nid_sig(nid3, sig);
goto okay;
}
if (cell->type.in("$_OAI4_", "$_AOI4_"))
{
int sid = get_bv_sid(1);
- int nid_a = get_sig_nid(cell->getPort("\\A"));
- int nid_b = get_sig_nid(cell->getPort("\\B"));
+ int nid_a = get_sig_nid(cell->getPort(ID::A));
+ int nid_b = get_sig_nid(cell->getPort(ID::B));
int nid_c = get_sig_nid(cell->getPort("\\C"));
int nid_d = get_sig_nid(cell->getPort("\\D"));
btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
btorf("%d or %d %d %d\n", nid2, sid, nid_c, nid_d);
btorf("%d and %d %d %d\n", nid3, sid, nid1, nid2);
- btorf("%d not %d %d\n", nid4, sid, nid3);
+ btorf("%d not %d %d %s\n", nid4, sid, nid3, getinfo(cell).c_str());
}
if (cell->type == "$_AOI4_") {
btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
btorf("%d and %d %d %d\n", nid2, sid, nid_c, nid_d);
btorf("%d or %d %d %d\n", nid3, sid, nid1, nid2);
- btorf("%d not %d %d\n", nid4, sid, nid3);
+ btorf("%d not %d %d %s\n", nid4, sid, nid3, getinfo(cell).c_str());
}
- SigSpec sig = sigmap(cell->getPort("\\Y"));
+ SigSpec sig = sigmap(cell->getPort(ID::Y));
add_nid_sig(nid4, sig);
goto okay;
}
log_assert(!btor_op.empty());
int width = 1;
- width = std::max(width, GetSize(cell->getPort("\\A")));
- width = std::max(width, GetSize(cell->getPort("\\B")));
+ width = std::max(width, GetSize(cell->getPort(ID::A)));
+ width = std::max(width, GetSize(cell->getPort(ID::B)));
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
int sid = get_bv_sid(1);
- int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
- int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+ int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
+ int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
int nid = next_nid++;
if (cell->type.in("$lt", "$le", "$ge", "$gt")) {
- btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b);
+ btorf("%d %c%s %d %d %d %s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
} else {
- btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
+ btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
}
- SigSpec sig = sigmap(cell->getPort("\\Y"));
+ SigSpec sig = sigmap(cell->getPort(ID::Y));
if (GetSize(sig) > 1) {
int sid = get_bv_sid(GetSize(sig));
if (cell->type == "$neg") btor_op = "neg";
log_assert(!btor_op.empty());
- int width = GetSize(cell->getPort("\\Y"));
- width = std::max(width, GetSize(cell->getPort("\\A")));
+ int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y)));
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
int sid = get_bv_sid(width);
- int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
+ int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
int nid = next_nid++;
- btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
+ btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
- SigSpec sig = sigmap(cell->getPort("\\Y"));
+ SigSpec sig = sigmap(cell->getPort(ID::Y));
if (GetSize(sig) < width) {
int sid = get_bv_sid(GetSize(sig));
log_assert(!btor_op.empty());
int sid = get_bv_sid(1);
- int nid_a = get_sig_nid(cell->getPort("\\A"));
- int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort("\\B")) : 0;
+ int nid_a = get_sig_nid(cell->getPort(ID::A));
+ int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort(ID::B)) : 0;
- if (GetSize(cell->getPort("\\A")) > 1) {
+ if (GetSize(cell->getPort(ID::A)) > 1) {
int nid_red_a = next_nid++;
btorf("%d redor %d %d\n", nid_red_a, sid, nid_a);
nid_a = nid_red_a;
}
- if (btor_op != "not" && GetSize(cell->getPort("\\B")) > 1) {
+ if (btor_op != "not" && GetSize(cell->getPort(ID::B)) > 1) {
int nid_red_b = next_nid++;
btorf("%d redor %d %d\n", nid_red_b, sid, nid_b);
nid_b = nid_red_b;
int nid = next_nid++;
if (btor_op != "not")
- btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
+ btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
else
- btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
+ btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
- SigSpec sig = sigmap(cell->getPort("\\Y"));
+ SigSpec sig = sigmap(cell->getPort(ID::Y));
if (GetSize(sig) > 1) {
int sid = get_bv_sid(GetSize(sig));
log_assert(!btor_op.empty());
int sid = get_bv_sid(1);
- int nid_a = get_sig_nid(cell->getPort("\\A"));
+ int nid_a = get_sig_nid(cell->getPort(ID::A));
int nid = next_nid++;
- btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
if (cell->type == "$reduce_xnor") {
int nid2 = next_nid++;
+ btorf("%d %s %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
btorf("%d not %d %d %d\n", nid2, sid, nid);
nid = nid2;
+ } else {
+ btorf("%d %s %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
}
- SigSpec sig = sigmap(cell->getPort("\\Y"));
+ SigSpec sig = sigmap(cell->getPort(ID::Y));
if (GetSize(sig) > 1) {
int sid = get_bv_sid(GetSize(sig));
goto okay;
}
- if (cell->type.in("$mux", "$_MUX_"))
+ if (cell->type.in("$mux", "$_MUX_", "$_NMUX_"))
{
- SigSpec sig_a = sigmap(cell->getPort("\\A"));
- SigSpec sig_b = sigmap(cell->getPort("\\B"));
- SigSpec sig_s = sigmap(cell->getPort("\\S"));
- SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+ SigSpec sig_a = sigmap(cell->getPort(ID::A));
+ SigSpec sig_b = sigmap(cell->getPort(ID::B));
+ SigSpec sig_s = sigmap(cell->getPort(ID::S));
+ SigSpec sig_y = sigmap(cell->getPort(ID::Y));
int nid_a = get_sig_nid(sig_a);
int nid_b = get_sig_nid(sig_b);
int sid = get_bv_sid(GetSize(sig_y));
int nid = next_nid++;
- btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a);
+
+ if (cell->type == "$_NMUX_") {
+ int tmp = nid;
+ nid = next_nid++;
+ btorf("%d ite %d %d %d %d\n", tmp, sid, nid_s, nid_b, nid_a);
+ btorf("%d not %d %d %s\n", nid, sid, tmp, getinfo(cell).c_str());
+ } else {
+ btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_s, nid_b, nid_a, getinfo(cell).c_str());
+ }
add_nid_sig(nid, sig_y);
goto okay;
if (cell->type == "$pmux")
{
- SigSpec sig_a = sigmap(cell->getPort("\\A"));
- SigSpec sig_b = sigmap(cell->getPort("\\B"));
- SigSpec sig_s = sigmap(cell->getPort("\\S"));
- SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+ SigSpec sig_a = sigmap(cell->getPort(ID::A));
+ SigSpec sig_b = sigmap(cell->getPort(ID::B));
+ SigSpec sig_s = sigmap(cell->getPort(ID::S));
+ SigSpec sig_y = sigmap(cell->getPort(ID::Y));
int width = GetSize(sig_a);
int sid = get_bv_sid(width);
int nid_b = get_sig_nid(sig_b.extract(i*width, width));
int nid_s = get_sig_nid(sig_s.extract(i));
int nid2 = next_nid++;
- btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid);
+ if (i == GetSize(sig_s)-1)
+ btorf("%d ite %d %d %d %d %s\n", nid2, sid, nid_s, nid_b, nid, getinfo(cell).c_str());
+ else
+ btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid);
nid = nid2;
}
goto okay;
}
- if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
+ if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N_", "$_FF_"))
{
SigSpec sig_d = sigmap(cell->getPort("\\D"));
SigSpec sig_q = sigmap(cell->getPort("\\Q"));
+ if (!info_filename.empty() && cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_"))
+ {
+ SigSpec sig_c = sigmap(cell->getPort(cell->type == "$dff" ? "\\CLK" : "\\C"));
+ int nid = get_sig_nid(sig_c);
+ bool negedge = false;
+
+ if (cell->type == "$_DFF_N_")
+ negedge = true;
+
+ if (cell->type == "$dff" && !cell->getParam("\\CLK_POLARITY").as_bool())
+ negedge = true;
+
+ info_clocks[nid] |= negedge ? 2 : 1;
+ }
+
IdString symbol;
if (sig_q.is_wire()) {
int nid_init_val = -1;
if (!initval.is_fully_undef())
- nid_init_val = get_sig_nid(initval);
+ nid_init_val = get_sig_nid(initval, -1, false, true);
int sid = get_bv_sid(GetSize(sig_q));
int nid = next_nid++;
if (cell->type.in("$anyconst", "$anyseq"))
{
- SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+ SigSpec sig_y = sigmap(cell->getPort(ID::Y));
int sid = get_bv_sid(GetSize(sig_y));
int nid = next_nid++;
if (cell->type == "$initstate")
{
- SigSpec sig_y = sigmap(cell->getPort("\\Y"));
+ SigSpec sig_y = sigmap(cell->getPort(ID::Y));
if (initstate_nid < 0)
{
int sid = get_bv_sid(1);
- int one_nid = get_sig_nid(Const(1, 1));
- int zero_nid = get_sig_nid(Const(0, 1));
+ int one_nid = get_sig_nid(State::S1);
+ int zero_nid = get_sig_nid(State::S0);
initstate_nid = next_nid++;
btorf("%d state %d\n", initstate_nid, sid);
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
{
if (verbose)
btorf("; initval = %s\n", log_signal(firstword));
- nid_init_val = get_sig_nid(firstword);
+ nid_init_val = get_sig_nid(firstword, -1, false, true);
}
else
{
- int nid_init_val = next_nid++;
+ nid_init_val = next_nid++;
btorf("%d state %d\n", nid_init_val, sid);
for (int i = 0; i < nwords; i++) {
if (thisword.is_fully_undef())
continue;
Const thisaddr(i, abits);
- int nid_thisword = get_sig_nid(thisword);
- int nid_thisaddr = get_sig_nid(thisaddr);
+ int nid_thisword = get_sig_nid(thisword, -1, false, true);
+ int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true);
int last_nid_init_val = nid_init_val;
nid_init_val = next_nid++;
if (verbose)
cell_recursion_guard.erase(cell);
}
- int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
+ int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false)
{
int nid = -1;
sigmap.apply(sig);
int sid = get_bv_sid(GetSize(sig));
int nid_input = next_nid++;
- btorf("%d input %d\n", nid_input, sid);
+ if (is_init)
+ btorf("%d state %d\n", nid_input, sid);
+ else
+ btorf("%d input %d\n", nid_input, sid);
int nid_masked_input;
if (sig_mask_undef.is_fully_ones()) {
else
{
if (bit_cell.count(bit) == 0)
- log_error("No driver for signal bit %s.\n", log_signal(bit));
- export_cell(bit_cell.at(bit));
- log_assert(bit_nid.count(bit));
+ {
+ SigSpec s = bit;
+
+ while (i+GetSize(s) < GetSize(sig) && sig[i+GetSize(s)].wire != nullptr &&
+ bit_cell.count(sig[i+GetSize(s)]) == 0)
+ s.append(sig[i+GetSize(s)]);
+
+ log_warning("No driver for signal %s.\n", log_signal(s));
+
+ int sid = get_bv_sid(GetSize(s));
+ int nid = next_nid++;
+ btorf("%d input %d\n", nid, sid);
+ nid_width[nid] = GetSize(s);
+
+ for (int j = 0; j < GetSize(s); j++)
+ nidbits.push_back(make_pair(nid, j));
+
+ i += GetSize(s)-1;
+ continue;
+ }
+ else
+ {
+ export_cell(bit_cell.at(bit));
+ log_assert(bit_nid.count(bit));
+ }
}
}
return nid;
}
- BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad) :
- f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad)
+ BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, string info_filename) :
+ f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad), cover_mode(cover_mode), info_filename(info_filename)
{
+ if (!info_filename.empty())
+ infof("name %s\n", log_id(module));
+
btorf_push("inputs");
for (auto wire : module->wires())
int sid = get_bv_sid(GetSize(sig));
int nid = next_nid++;
- btorf("%d input %d %s\n", nid, sid, log_id(wire));
+ btorf("%d input %d %s\n", nid, sid, getinfo(wire).c_str());
add_nid_sig(nid, sig);
}
btorf_push(stringf("output %s", log_id(wire)));
int nid = get_sig_nid(wire);
- btorf("%d output %d %s\n", next_nid++, nid, log_id(wire));
+ btorf("%d output %d %s\n", next_nid++, nid, getinfo(wire).c_str());
btorf_pop(stringf("output %s", log_id(wire)));
}
btorf_push(log_id(cell));
int sid = get_bv_sid(1);
- int nid_a = get_sig_nid(cell->getPort("\\A"));
+ int nid_a = get_sig_nid(cell->getPort(ID::A));
int nid_en = get_sig_nid(cell->getPort("\\EN"));
int nid_not_en = next_nid++;
int nid_a_or_not_en = next_nid++;
btorf_push(log_id(cell));
int sid = get_bv_sid(1);
- int nid_a = get_sig_nid(cell->getPort("\\A"));
+ int nid_a = get_sig_nid(cell->getPort(ID::A));
int nid_en = get_sig_nid(cell->getPort("\\EN"));
int nid_not_a = next_nid++;
int nid_en_and_not_a = next_nid++;
btorf("%d not %d %d\n", nid_not_a, sid, nid_a);
btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a);
- if (single_bad) {
+ if (single_bad && !cover_mode) {
bad_properties.push_back(nid_en_and_not_a);
+ } else {
+ if (cover_mode) {
+ infof("bad %d %s\n", nid_en_and_not_a, getinfo(cell, true).c_str());
+ } else {
+ int nid = next_nid++;
+ btorf("%d bad %d %s\n", nid, nid_en_and_not_a, getinfo(cell, true).c_str());
+ }
+ }
+
+ btorf_pop(log_id(cell));
+ }
+
+ if (cell->type == "$cover" && cover_mode)
+ {
+ btorf_push(log_id(cell));
+
+ int sid = get_bv_sid(1);
+ int nid_a = get_sig_nid(cell->getPort("\\A"));
+ int nid_en = get_sig_nid(cell->getPort("\\EN"));
+ int nid_en_and_a = next_nid++;
+
+ btorf("%d and %d %d %d\n", nid_en_and_a, sid, nid_en, nid_a);
+
+ if (single_bad) {
+ bad_properties.push_back(nid_en_and_a);
} else {
int nid = next_nid++;
- btorf("%d bad %d\n", nid, nid_en_and_not_a);
+ btorf("%d bad %d %s\n", nid, nid_en_and_a, getinfo(cell, true).c_str());
}
btorf_pop(log_id(cell));
continue;
int this_nid = next_nid++;
- btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, log_id(wire));
+ btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, getinfo(wire).c_str());
btorf_pop(stringf("wire %s", log_id(wire)));
continue;
}
int nid2 = next_nid++;
- btorf("%d next %d %d %d\n", nid2, sid, nid, nid_head);
+ btorf("%d next %d %d %d %s\n", nid2, sid, nid, nid_head, getinfo(cell).c_str());
}
else
{
SigSpec sig = sigmap(cell->getPort("\\D"));
int nid_q = get_sig_nid(sig);
int sid = get_bv_sid(GetSize(sig));
- btorf("%d next %d %d %d\n", next_nid++, sid, nid, nid_q);
+ btorf("%d next %d %d %d %s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str());
}
btorf_pop(stringf("next %s", log_id(cell)));
btorf("%d bad %d\n", nid, todo[cursor]);
}
}
+
+ if (!info_filename.empty())
+ {
+ for (auto &it : info_clocks)
+ {
+ switch (it.second)
+ {
+ case 1:
+ infof("posedge %d\n", it.first);
+ break;
+ case 2:
+ infof("negedge %d\n", it.first);
+ break;
+ case 3:
+ infof("event %d\n", it.first);
+ break;
+ default:
+ log_abort();
+ }
+ }
+
+ std::ofstream f;
+ f.open(info_filename.c_str(), std::ofstream::trunc);
+ if (f.fail())
+ log_error("Can't open file `%s' for writing: %s\n", info_filename.c_str(), strerror(errno));
+ for (auto &it : info_lines)
+ f << it;
+ f.close();
+ }
}
};
log(" -s\n");
log(" Output only a single bad property for all asserts\n");
log("\n");
+ log(" -c\n");
+ log(" Output cover properties using 'bad' statements instead of asserts\n");
+ log("\n");
+ log(" -i <filename>\n");
+ log(" Create additional info file with auxiliary information\n");
+ log("\n");
}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
- bool verbose = false, single_bad = false;
+ bool verbose = false, single_bad = false, cover_mode = false;
+ string info_filename;
log_header(design, "Executing BTOR backend.\n");
single_bad = true;
continue;
}
+ if (args[argidx] == "-c") {
+ cover_mode = true;
+ continue;
+ }
+ if (args[argidx] == "-i" && argidx+1 < args.size()) {
+ info_filename = args[++argidx];
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
*f << stringf("; BTOR description generated by %s for module %s.\n",
yosys_version_str, log_id(topmod));
- BtorWorker(*f, topmod, verbose, single_bad);
+ BtorWorker(*f, topmod, verbose, single_bad, cover_mode, info_filename);
*f << stringf("; end of yosys output\n");
}
projects / yosys.git / blobdiff