riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Improve BTOR2 handling of undriven wires 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2019-06-26 17:42:00 +02:00
parent f6053b8810
commit 1b49380f6b
1 changed files with 27 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
backends/btor/btor.cc
View File

@ -17,6 +17,11 @@
* *
*/ */
// [[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/rtlil.h"
#include "kernel/register.h" #include "kernel/register.h"
#include "kernel/sigtools.h" #include "kernel/sigtools.h"
@ -875,9 +880,28 @@ struct BtorWorker
else else
{ {
if (bit_cell.count(bit) == 0) if (bit_cell.count(bit) == 0)
log_error("No driver for signal bit %s.\n", log_signal(bit)); {
export_cell(bit_cell.at(bit)); SigSpec s = bit;
log_assert(bit_nid.count(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 %s\n", nid, sid);
nid_width[nid] = GetSize(s);
i += GetSize(s)-1;
continue;
}
else
{
export_cell(bit_cell.at(bit));
log_assert(bit_nid.count(bit));
}
} }
} }