YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
387 stars 73 forks source link

translate backslashes in cell names the same way as smt2 backend does #142

Closed nakengelhardt closed 2 years ago

nakengelhardt commented 2 years ago

Backslashes are not allowed in smt2 format, so the smt2 backend translates them to forward slashes. This prevents sby from finding the corresponding cell in the json export. Apply the same transformation when looking up the property cellname.

nakengelhardt commented 2 years ago

There's still a weakness here where it cannot disambiguate signal names that are identical except for \|/ characters, but this is a bug people are currently running into so merging this to at least mostly fix it.