From fcf9f9eb66a3a1989ce6bf87402dd1dd97a768eb Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 13 Mar 2024 06:44:52 +1300 Subject: [PATCH] btor2aiger: Use ywa inits list `btor2aiger` tool restarts latch indexing at 0 but aiw2yw expects index to be unique. Offset latch input number by the total input count to fix this. --- tools/btor2aig_yw/btor2aig_yw.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py index 3fe4f3a7..19fc7b6e 100644 --- a/tools/btor2aig_yw/btor2aig_yw.py +++ b/tools/btor2aig_yw/btor2aig_yw.py @@ -82,12 +82,14 @@ async def main() -> None: pattern = r"(?P[cil])(?P\d+) (?P.*?)(\[(?P\d+)\])?$" m = re.match(pattern, string) md = m.groupdict() + md['input'] = int(md['input']) if md['type'] == 'i': md['type'] = 'input' elif md['type'] == 'c': md['type'] = 'clk' elif md['type'] == 'l': md['type'] = 'latch' + md['input'] += ywa['input_count'] else: raise ValueError(f"Unknown type identifier {md['type']!r}") for k in ['input', 'offset']: @@ -109,7 +111,7 @@ async def main() -> None: elif md_type == 'input': ywa['inputs'].append(md) elif md_type == 'latch': - ywa['latches'].append(md) + ywa['inits'].append(md) # get next line data = await proc.stdout.readline()