Skip to content

Commit

Permalink
Merge pull request #298 from YosysHQ/george/smtbmc_paths
Browse files Browse the repository at this point in the history
smtbmc: match on full property paths instead of just names
  • Loading branch information
jix authored Oct 7, 2024
2 parents 62d1708 + 9583985 commit 117fb26
Show file tree
Hide file tree
Showing 3 changed files with 42 additions and 34 deletions.
42 changes: 18 additions & 24 deletions sbysrc/sby_design.py
Original file line number Diff line number Diff line change
Expand Up @@ -139,32 +139,26 @@ def __iter__(self):
def get_property_list(self):
return [p for p in self if p.type != p.Type.ASSUME]

def find_property(self, hierarchy, location):
# FIXME: use that RE that works with escaped paths from https://stackoverflow.com/questions/46207665/regex-pattern-to-split-verilog-path-in-different-instances-using-python
path = hierarchy.split('.')
mod = path.pop(0)
if self.name != mod:
raise ValueError(f"{self.name} is not the first module in hierarchical path {hierarchy}.")
try:
mod_hier = self
while path:
mod = path.pop(0)
mod_hier = mod_hier.submodules[mod]
except KeyError:
raise KeyError(f"Could not find {hierarchy} in design hierarchy!")
try:
prop = next(p for p in mod_hier.properties if location in p.location)
except StopIteration:
raise KeyError(f"Could not find assert at {location} in properties list!")
return prop

def find_property_by_cellname(self, cell_name, trans_dict=dict()):
def find_property(self, path, cell_name, trans_dict=dict()):
# backends may need to mangle names irreversibly, so allow applying
# the same transformation here
for prop in self:
if cell_name == prop.name.translate(str.maketrans(trans_dict)):
return prop
raise KeyError(f"No such property: {cell_name}")
trans = str.maketrans(trans_dict)
path_iter = iter(path)

mod = next(path_iter).translate(trans)
if self.name != mod:
raise ValueError(f"{self.name} is not the first module in hierarchical path {pretty_path(path)}.")

mod_hier = self
for mod in path_iter:
mod_hier = next((v for k, v in mod_hier.submodules.items() if mod == k.translate(trans)), None)
if not mod_hier:
raise KeyError(f"Could not find {pretty_path(path)} in design hierarchy!")

prop = next((p for p in mod_hier.properties if cell_name == p.name.translate(trans)), None)
if not prop:
raise KeyError(f"Could not find property {cell_name} at location {pretty_print(path)} in properties list!")
return prop


@dataclass
Expand Down
10 changes: 8 additions & 2 deletions sbysrc/sby_engine_aiger.py
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,11 @@ def output_callback2(line):

smt2_trans = {'\\':'/', '|':'/'}

def parse_mod_path(path_string):
# Match a path with . as delimiter, allowing escaped tokens in
# verilog `\name ` format
return [m[1] or m[0] for m in re.findall(r"(\\([^ ]*) |[^\.]+)(?:\.|$)", path_string)]

match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line)
if match:
current_step = int(match[1])
Expand All @@ -213,10 +218,11 @@ def output_callback2(line):
match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
if match: proc2_status = "PASS"

match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+)(?: \((\S+)\))?", line)
match = re.match(r"^## [0-9: ]+ Assert failed in ([^:]+): (\S+)(?: \((\S+)\))?", line)
if match:
path = parse_mod_path(match[1])
cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
prop.status = "FAIL"
task.status_db.set_task_property_status(prop, data=dict(source="aigsmt", engine=f"engine_{engine_idx}"))
last_prop.append(prop)
Expand Down
24 changes: 16 additions & 8 deletions sbysrc/sby_engine_smtbmc.py
Original file line number Diff line number Diff line change
Expand Up @@ -203,6 +203,11 @@ def output_callback(line):

smt2_trans = {'\\':'/', '|':'/'}

def parse_mod_path(path_string):
# Match a path with . as delimiter, allowing escaped tokens in
# verilog `\name ` format
return [m[1] or m[0] for m in re.findall(r"(\\([^ ]*) |[^\.]+)(?:\.|$)", path_string)]

match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line)
if match:
current_step = int(match[1])
Expand All @@ -228,19 +233,21 @@ def output_callback(line):
proc_status = "ERROR"
return line

match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+)(?: \((\S+)\))?", line)
match = re.match(r"^## [0-9: ]+ Assert failed in ([^:]+): (\S+)(?: \((\S+)\))?", line)
if match:
path = parse_mod_path(match[1])
cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
prop.status = "FAIL"
task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))
last_prop.append(prop)
return line

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 in step \d+ at ([^:]+): (\S+)(?: \((\S+)\))?", line)
if match:
cell_name = match[2] or match[1]
prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
path = parse_mod_path(match[1])
cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
prop.status = "PASS"
task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))
last_prop.append(prop)
Expand Down Expand Up @@ -268,10 +275,11 @@ def output_callback(line):
tracefile = match[1]
pending_sim = tracefile

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:
cell_name = match[2]
prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
path = parse_mod_path(match[1])
cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
prop.status = "FAIL"
task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}"))

Expand Down

0 comments on commit 117fb26

Please sign in to comment.