Skip to content

Commit

Permalink
btor2aiger: Use ywa inits list
Browse files Browse the repository at this point in the history
`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.
  • Loading branch information
KrystalDelusion committed Mar 12, 2024
1 parent 5c762ad commit fcf9f9e
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion tools/btor2aig_yw/btor2aig_yw.py
Original file line number Diff line number Diff line change
Expand Up @@ -82,12 +82,14 @@ async def main() -> None:
pattern = r"(?P<type>[cil])(?P<input>\d+) (?P<path>.*?)(\[(?P<offset>\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']:
Expand All @@ -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()
Expand Down

0 comments on commit fcf9f9e

Please sign in to comment.