mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-10-31 04:52:30 +00:00
Code Activity

Merge pull request #142 from nakengelhardt/fix_backslash_smt2

Browse source 
translate backslashes in cell names the same way as smt2 backend does
This commit is contained in:
N. Engelhardt 2022-03-28 16:32:10 +02:00 • committed by GitHub
commit 3d8f56b89a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
sbysrc/sby_design.py
View file

@ -91,11 +91,13 @@ class SbyModule:
raise KeyError(f"Could not find assert at {location} in properties list!") raise KeyError(f"Could not find assert at {location} in properties list!")
return prop return prop
def find_property_by_cellname(self, cell_name): def find_property_by_cellname(self, cell_name, trans_dict=dict()):
# backends may need to mangle names irreversibly, so allow applying
# the same transformation here
for prop in self: for prop in self:
if prop.name == cell_name: if cell_name == prop.name.translate(str.maketrans(trans_dict)):
return prop return prop
raise KeyError(f"No such property: {cell_name}") raise KeyError(f"No such property: {smt2_name}")
def design_hierarchy(filename): def design_hierarchy(filename):
design_json = json.load(filename) design_json = json.load(filename)

7
sbysrc/sby_engine_smtbmc.py
View file

@ -160,6 +160,7 @@ def run(mode, task, engine_idx, engine):
def output_callback(line): def output_callback(line):
nonlocal proc_status nonlocal proc_status
nonlocal last_prop nonlocal last_prop
smt2_trans = {'\\':'/', '|':'/'}
match = re.match(r"^## [0-9: ]+ Status: FAILED", line) match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
if match: if match:
@ -184,7 +185,7 @@ def run(mode, task, engine_idx, engine):
match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line) match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line)
if match: if match:
cell_name = match[3] cell_name = match[3]
prop = task.design_hierarchy.find_property_by_cellname(cell_name) prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "FAIL" prop.status = "FAIL"
last_prop = prop last_prop = prop
return line return line
@ -192,7 +193,7 @@ def run(mode, task, engine_idx, engine):
match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line) match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line)
if match: if match:
cell_name = match[2] cell_name = match[2]
prop = task.design_hierarchy.find_property_by_cellname(cell_name) prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "PASS" prop.status = "PASS"
last_prop = prop last_prop = prop
return line return line
@ -206,7 +207,7 @@ def run(mode, task, engine_idx, engine):
match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line) match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line)
if match: if match:
cell_name = match[2] cell_name = match[2]
prop = task.design_hierarchy.find_property_by_cellname(cell_name) prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "FAIL" prop.status = "FAIL"
return line return line

3
tests/submod_props.sby
View file

@ -1,10 +1,12 @@
[tasks] [tasks]
bmc bmc
cover cover
flatten
[options] [options]
bmc: mode bmc bmc: mode bmc
cover: mode cover cover: mode cover
flatten: mode bmc
expect fail expect fail
@ -14,6 +16,7 @@ smtbmc boolector
[script] [script]
read -sv test.sv read -sv test.sv
prep -top top prep -top top
flatten: flatten
[file test.sv] [file test.sv]
module test(input foo); module test(input foo);