fix induction

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 7535d71596ba901ba1f219e9c3f7543577a8b452..ede1a8d968fb309d7d747531a0ec980b62ffe043 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/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)

diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py
index c0fdb8b6880175a241c520f1cb9f8aa945f3413b..98a57f132b16c1c733c1234ace39b1e1f450d312 100644 (file)
--- a/sbysrc/sby_design.py
+++ b/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
 

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 0bf887d49b2a846c6734045eb9b4c100cbfede00..492e2a57f01a248c97ec39cb698bfc1b334c4de5 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/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()

diff --git a/tests/both_ex.sby b/tests/both_ex.sby
index f83f2b172e16beb681bf3899c05b0ade7007447e..81773747df69b7a751c354e272d3484736b10f5b 100644 (file)
--- a/tests/both_ex.sby
+++ b/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]

diff --git a/tests/cover_fail.sby b/tests/cover_fail.sby
index f75a91112fa79e0d2a21148ff698fe0bb4cdcd88..8031e207ee3b12fc77580e649961569ec5c384a8 100644 (file)
--- a/tests/cover_fail.sby
+++ b/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]

diff --git a/tests/multi_assert.sby b/tests/multi_assert.sby
index 818195f8644f434300d33063735d5d1b23197b56..883181a8a23311ff804682f93d2737f8e6a7005d 100644 (file)
--- a/tests/multi_assert.sby
+++ b/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]

diff --git a/tests/preunsat.sby b/tests/preunsat.sby
index 6694a6c35ab23e4904891074e1f6c1c2f073d851..98255c616727b2cf62d592695e1485deb69c779a 100644 (file)
--- a/tests/preunsat.sby
+++ b/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]

diff --git a/tests/redxor.sby b/tests/redxor.sby
index 6e6e9f8b95f20f83acce49d916caf0ec79a1e86d..0746861e95a03fcc551122887e340647b0f178e7 100644 (file)
--- a/tests/redxor.sby
+++ b/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]

diff --git a/tests/stopfirst.sby b/tests/stopfirst.sby
index 35ed539c8e59954186f7543ab2f54143ab382f35..782f79199efdb6681ab57595e6c755b4942e6e47 100644 (file)
--- a/tests/stopfirst.sby
+++ b/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]

diff --git a/tests/submod_props.sby b/tests/submod_props.sby
index 33a3a006976f6c37fac35a953bf13a9465a59b02..93abc9c139d18ca8d8fe07d943e7f63acec99fec 100644 (file)
--- a/tests/submod_props.sby
+++ b/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]