fix induction

sbysrc/sby_core.py

@@ -773,7 +773,7 @@ class SbyTask:
             junit_skipped = 0
         print(f'<?xml version="1.0" encoding="UTF-8"?>', file=f)
         print(f'<testsuites>', file=f)
-        print(f'<testsuite timestamp="{junit_time}" hostname="{platform.node()}" package="{junit_ts_name}" id="1" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{self.total_time}" skipped="{junit_skipped}">', file=f)
+        print(f'<testsuite timestamp="{junit_time}" hostname="{platform.node()}" package="{junit_ts_name}" id="0" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{self.total_time}" skipped="{junit_skipped}">', file=f)
         print(f'<properties>', file=f)
         print(f'<property name="os" value="{platform.system()}"/>', file=f)
         print(f'</properties>', file=f)

sbysrc/sby_design.py

@@ -51,7 +51,7 @@ class SbyProperty:
     tracefile: str = field(default="")
 
     def __repr__(self):
-        return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\""
+        return f"SbyProperty<{self.type} {self.name} at {self.location}: status={self.status}, tracefile=\"{self.tracefile}\">"
 
 @dataclass
 class SbyModule:
@@ -105,14 +105,15 @@ def design_hierarchy(filename):
 
         cells = design_json["modules"][module_name]["cells"]
         for cell_name, cell in cells.items():
+            sub_hierarchy=f"{hierarchy}/{instance_name}" if hierarchy else instance_name
             if cell["type"][0] != '$':
-                mod.submodules[cell_name] = make_mod_hier(cell_name, cell["type"], hierarchy=f"{hierarchy}/{instance_name}")
+                mod.submodules[cell_name] = make_mod_hier(cell_name, cell["type"], hierarchy=sub_hierarchy)
             if cell["type"] in ["$assume", "$assert", "$cover", "$live"]:
                 try:
                     location = cell["attributes"]["src"]
                 except KeyError:
                     location = ""
-                p = SbyProperty(name=cell_name, type=SbyProperty.Type.from_cell(cell["type"]), location=location, hierarchy=f"{hierarchy}/{instance_name}")
+                p = SbyProperty(name=cell_name, type=SbyProperty.Type.from_cell(cell["type"]), location=location, hierarchy=sub_hierarchy)
                 mod.properties.append(p)
         return mod
 

sbysrc/sby_engine_smtbmc.py

@@ -273,6 +273,9 @@ def run(mode, task, engine_idx, engine):
                 assert False
 
             if task.basecase_pass and task.induction_pass:
+                for prop in task.design_hierarchy:
+                    if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN":
+                        prop.status = "PASS"
                 task.update_status("PASS")
                 task.summary.append("successful proof by k-induction.")
                 task.terminate()

tests/both_ex.sby

@@ -15,7 +15,7 @@ pono: btor pono
 cover: btor btormc
 
 [script]
-read_verilog -sv both_ex.v
+read -sv both_ex.v
 prep -top test
 
 [files]

tests/cover_fail.sby

@@ -7,7 +7,7 @@ expect fail
 smtbmc boolector
 
 [script]
-read_verilog -sv test.v
+read -sv test.v
 prep -top test
 
 [file test.v]

tests/multi_assert.sby

@@ -12,7 +12,7 @@ btormc: btor btormc
 pono: btor pono
 
 [script]
-read_verilog -sv multi_assert.v
+read -sv multi_assert.v
 prep -top test
 
 [file multi_assert.v]

tests/preunsat.sby

@@ -12,7 +12,7 @@ btormc: btor btormc
 yices: smtbmc yices
 
 [script]
-read_verilog -sv test.sv
+read -sv test.sv
 prep -top test
 
 [file test.sv]

tests/redxor.sby

@@ -6,7 +6,7 @@ expect pass
 btor btormc
 
 [script]
-read_verilog -formal redxor.v
+read -formal redxor.v
 prep -top test
 
 [files]

tests/stopfirst.sby

@@ -6,7 +6,7 @@ expect fail
 btor btormc
 
 [script]
-read_verilog -sv test.sv
+read -sv test.sv
 prep -top test
 
 [file test.sv]

tests/submod_props.sby

@@ -12,7 +12,7 @@ expect fail
 smtbmc boolector
 
 [script]
-read_verilog -sv test.sv
+read -sv test.sv
 prep -top top
 
 [file test.sv]