From b88d2e5f30712f797a5c4fb2b7308494155b95d0 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 18 Sep 2019 11:56:14 +0200 Subject: Fix stupid bug in btor back-end Signed-off-by: Clifford Wolf --- backends/btor/btor.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 7c054d655..4472993d4 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -685,7 +685,7 @@ struct BtorWorker } 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++) { -- cgit v1.2.3 From 5eebfabe4286d47a75508677e2bc76e8b422a879 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Fri, 27 Sep 2019 12:40:17 -0400 Subject: Corrects btor2 backend --- backends/btor/btor.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 4472993d4..f617b7ec2 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -897,9 +897,12 @@ struct BtorWorker int sid = get_bv_sid(GetSize(s)); int nid = next_nid++; - btorf("%d input %d %s\n", nid, sid); + 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; } -- cgit v1.2.3 From a84a2d74c779b8023c0bbfc02fa4576d8c4cecca Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 2 Oct 2019 12:48:04 +0200 Subject: Fix btor back-end to use "state" instead of "input" for undef init bits Signed-off-by: Clifford Wolf --- backends/btor/btor.cc | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'backends/btor/btor.cc') diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index f617b7ec2..9e316a055 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -569,7 +569,7 @@ struct BtorWorker 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++; @@ -681,7 +681,7 @@ struct BtorWorker { 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 { @@ -693,8 +693,8 @@ struct BtorWorker 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) @@ -792,7 +792,7 @@ struct BtorWorker 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); @@ -823,7 +823,10 @@ struct BtorWorker 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()) { -- cgit v1.2.3