From 4cccbf77fa7f3e7df0c3d12993fb4edda869461e Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 31 Mar 2022 08:50:49 -0400
Subject: [PATCH 01/22] sby: core: Added preliminary support for the `[setup]`
 section

---
 sbysrc/sby_core.py | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 366817f..599e7bc 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -247,6 +247,7 @@ class SbyConfig:
     def __init__(self):
         self.options = dict()
         self.engines = list()
+        self.setup = dict()
         self.script = list()
         self.autotune_config = None
         self.files = dict()
@@ -294,6 +295,12 @@ class SbyConfig:
                         self.error(f"sby file syntax error: '[engines]' section does not accept any arguments. got {args}")
                     continue
 
+                if entries[0] == "setup":
+                    mode = "setup"
+                    if len(self.setup) != 0 or len(entries) != 1:
+                        self.error(f"sby file syntax error: {line}")
+                    continue
+
                 if section == "script":
                     mode = "script"
                     if len(self.script) != 0:
@@ -351,6 +358,28 @@ class SbyConfig:
                 self.engines.append(entries)
                 continue
 
+            if mode == "setup":
+                self.error("[setup] section not yet supported")
+                kvp = line.split()
+                if kvp[0] not in ("cutpoint", "disable", "enable", "assume", "define"):
+                    self.error(f"sby file syntax error: {line}")
+                else:
+                    stmt = kvp[0]
+                    if stmt == 'define':
+                        if 'define' not in self.setup:
+                            self.setup['define'] = {}
+
+                        if len(kvp[1:]) < 2:
+                            self.error(f"sby file syntax error: {line}")
+                        elif kvp[1][0] != '@':
+                            self.error(f"sby file syntax error: {line}")
+                        else:
+                            name = kvp[1][1:]
+                            self.setup['define'][name] = kvp[2:]
+                    else:
+                        self.setup[key] = kvp[1:]
+                continue
+
             if mode == "script":
                 self.script.append(line)
                 continue

From ed82c78accdf25dc2e249ec4249fd9f86dcb907f Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 31 Mar 2022 10:06:02 -0400
Subject: [PATCH 02/22] sby: core: Added preliminary support for `[stage]`
 sections

---
 sbysrc/sby_core.py | 56 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 56 insertions(+)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 599e7bc..b12723e 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -248,6 +248,7 @@ class SbyConfig:
         self.options = dict()
         self.engines = list()
         self.setup = dict()
+        self.stage = dict()
         self.script = list()
         self.autotune_config = None
         self.files = dict()
@@ -301,6 +302,27 @@ class SbyConfig:
                         self.error(f"sby file syntax error: {line}")
                     continue
 
+                if entries[0] == "stage":
+                    mode = "stage"
+                    if len(entries) > 3 or len(entries) < 2:
+                        self.error(f"sby file syntax error: {line}")
+
+                    if len(entries) == 2:
+                        parent = None
+                    else:
+                        parent = entries[2]
+
+                    key = entries[1]
+
+                    if key in self.stage:
+                        self.error(f"stage {key} already defined")
+
+                    self.stage[key] = {
+                        'parent': parent
+                    }
+
+                    continue
+
                 if section == "script":
                     mode = "script"
                     if len(self.script) != 0:
@@ -380,6 +402,35 @@ class SbyConfig:
                         self.setup[key] = kvp[1:]
                 continue
 
+                if mode == "stage":
+                    self.error("[stage] section not yet supported")
+                    kvp = line.split()
+                    if key is None or key == '':
+                        self.error(f"sby file syntax error: in stage mode but unknown key")
+
+                    if len(kvp) == 0:
+                        continue
+
+                    if kvp[0] not in ("mode", "depth", "timeout", "expect", "engine",
+                                      "cutpoint", "enable", "disable", "assume", "skip",
+                                      "check", "prove", "abstract", "setsel") or len(kvp) < 2:
+                        self.error(f"sby file syntax error: {line}")
+                    else:
+                        stmt = kvp[0]
+                        if stmt == 'setsel':
+                            if len(kvp[1:]) < 2:
+                                self.error(f"sby file syntax error: {line}")
+                            elif kvp[1][0] != '@':
+                                self.error(f"sby file syntax error: {line}")
+                            else:
+                                name = kvp[1][1:]
+                                self.stage[key][stmt] = {
+                                    'name': name, 'pattern': kvp[2:]
+                                }
+                        else:
+                            self.stage[key][stmt] = kvp[1:]
+                    continue
+
             if mode == "script":
                 self.script.append(line)
                 continue
@@ -834,6 +885,11 @@ class SbyTask(SbyConfig):
         with open(f"{self.workdir}/config.sby", "r") as f:
             self.parse_config(f)
 
+        if len(self.stage) == 0:
+            self.stage['default'] = {
+                'enable', '*'
+            }
+
         self.handle_str_option("mode", None)
 
         if self.opt_mode not in ["bmc", "prove", "cover", "live"]:

From 0ab158eea1de1b24afd9d66f0a95864934f2ea4a Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Tue, 28 Jun 2022 22:54:49 -0400
Subject: [PATCH 03/22] sby: core: minor update to the stage parsing

---
 sbysrc/sby_core.py | 52 +++++++++++++++++++++++-----------------------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index b12723e..9264569 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -399,38 +399,38 @@ class SbyConfig:
                             name = kvp[1][1:]
                             self.setup['define'][name] = kvp[2:]
                     else:
-                        self.setup[key] = kvp[1:]
+                        self.setup[stmt] = kvp[1:]
                 continue
 
-                if mode == "stage":
+            if mode == "stage":
                     self.error("[stage] section not yet supported")
-                    kvp = line.split()
-                    if key is None or key == '':
-                        self.error(f"sby file syntax error: in stage mode but unknown key")
+                kvp = line.split()
+                if key is None or key == '':
+                    self.error(f"sby file syntax error: in stage mode but unknown key")
 
-                    if len(kvp) == 0:
-                        continue
-
-                    if kvp[0] not in ("mode", "depth", "timeout", "expect", "engine",
-                                      "cutpoint", "enable", "disable", "assume", "skip",
-                                      "check", "prove", "abstract", "setsel") or len(kvp) < 2:
-                        self.error(f"sby file syntax error: {line}")
-                    else:
-                        stmt = kvp[0]
-                        if stmt == 'setsel':
-                            if len(kvp[1:]) < 2:
-                                self.error(f"sby file syntax error: {line}")
-                            elif kvp[1][0] != '@':
-                                self.error(f"sby file syntax error: {line}")
-                            else:
-                                name = kvp[1][1:]
-                                self.stage[key][stmt] = {
-                                    'name': name, 'pattern': kvp[2:]
-                                }
-                        else:
-                            self.stage[key][stmt] = kvp[1:]
+                if len(kvp) == 0:
                     continue
 
+                if kvp[0] not in ("mode", "depth", "timeout", "expect", "engine",
+                                  "cutpoint", "enable", "disable", "assume", "skip",
+                                  "check", "prove", "abstract", "setsel") or len(kvp) < 2:
+                    self.error(f"sby file syntax error: {line}")
+                else:
+                    stmt = kvp[0]
+                    if stmt == 'setsel':
+                        if len(kvp[1:]) < 2:
+                            self.error(f"sby file syntax error: {line}")
+                        elif kvp[1][0] != '@':
+                            self.error(f"sby file syntax error: {line}")
+                        else:
+                            name = kvp[1][1:]
+                            self.stage[key][stmt] = {
+                                'name': name, 'pattern': kvp[2:]
+                            }
+                    else:
+                        self.stage[key][stmt] = kvp[1:]
+                continue
+
             if mode == "script":
                 self.script.append(line)
                 continue

From a0d366e58a94e163c6cb9f097727ce000681d182 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Fri, 29 Jul 2022 09:21:45 -0400
Subject: [PATCH 04/22] some cleanup, added some rough parser tests, and
 started altering the engines section

---
 sbysrc/sby_core.py       | 25 +++++++++++++++++--------
 tests/parser/.gitignore  |  4 ++++
 tests/parser/Makefile    |  2 ++
 tests/parser/engines.sby | 13 +++++++++++++
 tests/parser/options.sby |  4 ++++
 tests/parser/setup.sby   |  8 ++++++++
 tests/parser/stage.sby   | 12 ++++++++++++
 7 files changed, 60 insertions(+), 8 deletions(-)
 create mode 100644 tests/parser/.gitignore
 create mode 100644 tests/parser/Makefile
 create mode 100644 tests/parser/engines.sby
 create mode 100644 tests/parser/options.sby
 create mode 100644 tests/parser/setup.sby
 create mode 100644 tests/parser/stage.sby

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 9264569..8f988a6 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -246,7 +246,8 @@ class SbyAbort(BaseException):
 class SbyConfig:
     def __init__(self):
         self.options = dict()
-        self.engines = list()
+        # Define a default case for the engine block
+        self.engines = list() # { None: list() }
         self.setup = dict()
         self.stage = dict()
         self.script = list()
@@ -257,6 +258,7 @@ class SbyConfig:
 
     def parse_config(self, f):
         mode = None
+        engine_mode = None
 
         for line in f:
             raw_line = line
@@ -290,18 +292,26 @@ class SbyConfig:
 
                 if section == "engines":
                     mode = "engines"
-                    if len(self.engines) != 0:
-                        self.error(f"sby file syntax error: '[engines]' section already defined")
-                    if args is not None:
-                        self.error(f"sby file syntax error: '[engines]' section does not accept any arguments. got {args}")
-                    continue
+                    if len(entries) > 2:
+                        self.error(f"sby file syntax error: [engine] sections expects at most 1 argument, got more '{line}'")
 
+                    if len(entries) == 2 and entries[1] not in ("bmc", "prove", "cover", "live"):
+                        self.error(f"sby file syntax error: Expected one of 'bmc, prove, cover, live' not '{entries[1]}'")
+                    elif len(entries) == 2:
+                        pass
+                        # if entries[1] not in self.engines:
+                        #     self.engines[entries[1]] = list()
+                        # else:
+                        #     self.error(f"Already defined engine block for mode '{entries[1]}'")
+
+                # [setup]
                 if entries[0] == "setup":
                     mode = "setup"
                     if len(self.setup) != 0 or len(entries) != 1:
                         self.error(f"sby file syntax error: {line}")
                     continue
 
+                # [stage <NAME> (PARENTS...)]
                 if entries[0] == "stage":
                     mode = "stage"
                     if len(entries) > 3 or len(entries) < 2:
@@ -377,11 +387,11 @@ class SbyConfig:
 
             if mode == "engines":
                 entries = line.split()
+                # self.engines[engine_mode].append(entries)
                 self.engines.append(entries)
                 continue
 
             if mode == "setup":
-                self.error("[setup] section not yet supported")
                 kvp = line.split()
                 if kvp[0] not in ("cutpoint", "disable", "enable", "assume", "define"):
                     self.error(f"sby file syntax error: {line}")
@@ -403,7 +413,6 @@ class SbyConfig:
                 continue
 
             if mode == "stage":
-                    self.error("[stage] section not yet supported")
                 kvp = line.split()
                 if key is None or key == '':
                     self.error(f"sby file syntax error: in stage mode but unknown key")
diff --git a/tests/parser/.gitignore b/tests/parser/.gitignore
new file mode 100644
index 0000000..b87b190
--- /dev/null
+++ b/tests/parser/.gitignore
@@ -0,0 +1,4 @@
+*
+!Makefile
+!.gitignore
+!*.sby
diff --git a/tests/parser/Makefile b/tests/parser/Makefile
new file mode 100644
index 0000000..7827c43
--- /dev/null
+++ b/tests/parser/Makefile
@@ -0,0 +1,2 @@
+SUBDIR=parser
+include ../make/subdir.mk
diff --git a/tests/parser/engines.sby b/tests/parser/engines.sby
new file mode 100644
index 0000000..2277151
--- /dev/null
+++ b/tests/parser/engines.sby
@@ -0,0 +1,13 @@
+[options]
+mode bmc
+depth 1
+expect error
+
+[engines]
+smtbmc
+
+[engines bmc]
+smtbmc
+
+[engines cover]
+smtbmc
diff --git a/tests/parser/options.sby b/tests/parser/options.sby
new file mode 100644
index 0000000..666953d
--- /dev/null
+++ b/tests/parser/options.sby
@@ -0,0 +1,4 @@
+[options]
+mode bmc
+depth 1
+expect error
diff --git a/tests/parser/setup.sby b/tests/parser/setup.sby
new file mode 100644
index 0000000..6ca49e3
--- /dev/null
+++ b/tests/parser/setup.sby
@@ -0,0 +1,8 @@
+[options]
+mode bmc
+depth 1
+expect error
+
+
+[setup]
+enable *
diff --git a/tests/parser/stage.sby b/tests/parser/stage.sby
new file mode 100644
index 0000000..b69a186
--- /dev/null
+++ b/tests/parser/stage.sby
@@ -0,0 +1,12 @@
+[options]
+mode bmc
+depth 1
+expect error
+
+
+[stage stage_1]
+mode prove
+depth 20
+timeout 60
+expect error
+enable *

From f1a645bb187c3b84b9a6910abd102672ce22302f Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Fri, 29 Jul 2022 09:28:37 -0400
Subject: [PATCH 05/22] sby: core: config: Updated the `[stage]` section to use
 commas for the parents

---
 sbysrc/sby_core.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 8f988a6..417548c 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -311,7 +311,7 @@ class SbyConfig:
                         self.error(f"sby file syntax error: {line}")
                     continue
 
-                # [stage <NAME> (PARENTS...)]
+                # [stage <NAME> (PARENTS,...)]
                 if entries[0] == "stage":
                     mode = "stage"
                     if len(entries) > 3 or len(entries) < 2:
@@ -320,7 +320,7 @@ class SbyConfig:
                     if len(entries) == 2:
                         parent = None
                     else:
-                        parent = entries[2]
+                        parent = entries[2].split(',')
 
                     key = entries[1]
 

From 9293081308c64027b2b27c594ac6f722bb78866e Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Fri, 29 Jul 2022 10:21:48 -0400
Subject: [PATCH 06/22] modified the mode runners to accept the modified engine
 layout in preperation for the per-mode engine sections

---
 sbysrc/sby_core.py       |  7 +++----
 sbysrc/sby_mode_bmc.py   |  9 +++++++--
 sbysrc/sby_mode_cover.py | 10 ++++++++--
 sbysrc/sby_mode_live.py  |  9 +++++++--
 sbysrc/sby_mode_prove.py |  9 +++++++--
 5 files changed, 32 insertions(+), 12 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 417548c..7651f09 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -247,7 +247,7 @@ class SbyConfig:
     def __init__(self):
         self.options = dict()
         # Define a default case for the engine block
-        self.engines = list() # { None: list() }
+        self.engines = { None: list() }
         self.setup = dict()
         self.stage = dict()
         self.script = list()
@@ -387,8 +387,7 @@ class SbyConfig:
 
             if mode == "engines":
                 entries = line.split()
-                # self.engines[engine_mode].append(entries)
-                self.engines.append(entries)
+                self.engines[engine_mode].append(entries)
                 continue
 
             if mode == "setup":
@@ -565,7 +564,7 @@ class SbyTask(SbyConfig):
                     print(line, file=f)
 
     def engine_list(self):
-        return list(enumerate(self.engines))
+        return list(enumerate(self.engines.items()))
 
     def check_timeout(self):
         if self.opt_timeout is not None:
diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index cc4eba7..e8f4f71 100644
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -24,10 +24,15 @@ def run(task):
     task.handle_int_option("append", 0)
     task.handle_str_option("aigsmt", "yices")
 
-    for engine_idx, engine in task.engine_list():
+    for engine_idx, engine_section in task.engine_list():
+        engine = engine_section[1][0]
+        engine_name = engine_section[0]
+        if engine_name is None:
+            engine_name = engine_idx
+
         assert len(engine) > 0
 
-        task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")
+        task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
         if engine[0] == "smtbmc":
diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py
index 8fb1da9..f918247 100644
--- a/sbysrc/sby_mode_cover.py
+++ b/sbysrc/sby_mode_cover.py
@@ -23,10 +23,16 @@ def run(task):
     task.handle_int_option("depth", 20)
     task.handle_int_option("append", 0)
 
-    for engine_idx, engine in task.engine_list():
+    for engine_idx, engine_section in task.engine_list():
+        engine = engine_section[1][0]
+        engine_name = engine_section[0]
+        if engine_name is None:
+            engine_name = engine_idx
+
+
         assert len(engine) > 0
 
-        task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")
+        task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
         if engine[0] == "smtbmc":
diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py
index 6746200..d713215 100644
--- a/sbysrc/sby_mode_live.py
+++ b/sbysrc/sby_mode_live.py
@@ -24,10 +24,15 @@ def run(task):
 
     task.status = "UNKNOWN"
 
-    for engine_idx, engine in task.engine_list():
+    for engine_idx, engine_section in task.engine_list():
+        engine = engine_section[1][0]
+        engine_name = engine_section[0]
+        if engine_name is None:
+            engine_name = engine_idx
+
         assert len(engine) > 0
 
-        task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")
+        task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
         if engine[0] == "aiger":
diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index 1f62bb9..c4dcb0d 100644
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -31,10 +31,15 @@ def run(task):
     task.basecase_procs = list()
     task.induction_procs = list()
 
-    for engine_idx, engine in task.engine_list():
+    for engine_idx, engine_section in task.engine_list():
+        engine = engine_section[1][0]
+        engine_name = engine_section[0]
+        if engine_name is None:
+            engine_name = engine_idx
+
         assert len(engine) > 0
 
-        task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")
+        task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
         if engine[0] == "smtbmc":

From 204869bfedbcaec09465580654367da50ba7c5de Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Fri, 29 Jul 2022 10:34:36 -0400
Subject: [PATCH 07/22] sby: core: config: updated the error messages for the
 new setctions to make them more descriptive

---
 sbysrc/sby_core.py | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 7651f09..d5de81f 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -393,7 +393,7 @@ class SbyConfig:
             if mode == "setup":
                 kvp = line.split()
                 if kvp[0] not in ("cutpoint", "disable", "enable", "assume", "define"):
-                    self.error(f"sby file syntax error: {line}")
+                    self.error(f"sby file syntax error: found '{kvp[0]}' but expected one of 'cutpoint', 'disable', 'enable', 'assume', or 'define'")
                 else:
                     stmt = kvp[0]
                     if stmt == 'define':
@@ -401,9 +401,9 @@ class SbyConfig:
                             self.setup['define'] = {}
 
                         if len(kvp[1:]) < 2:
-                            self.error(f"sby file syntax error: {line}")
+                            self.error(f"sby file syntax error: 'define' statement takes 2 arguments, got {len(kvp[1:])}")
                         elif kvp[1][0] != '@':
-                            self.error(f"sby file syntax error: {line}")
+                            self.error(f"sby file syntax error: 'define' statement expects an '@' prefixed name as the first parameter, got {line}")
                         else:
                             name = kvp[1][1:]
                             self.setup['define'][name] = kvp[2:]
@@ -427,9 +427,9 @@ class SbyConfig:
                     stmt = kvp[0]
                     if stmt == 'setsel':
                         if len(kvp[1:]) < 2:
-                            self.error(f"sby file syntax error: {line}")
+                            self.error(f"sby file syntax error: 'setsel' statement takes 2 arguments, got {len(kvp[1:])}")
                         elif kvp[1][0] != '@':
-                            self.error(f"sby file syntax error: {line}")
+                            self.error(f"sby file syntax error: 'setsel' statement expects an '@' prefixed name as the first parameter, got {line}")
                         else:
                             name = kvp[1][1:]
                             self.stage[key][stmt] = {

From 4abd8a7d6944e48b96fcddd193f850852baa20c7 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Fri, 29 Jul 2022 10:50:57 -0400
Subject: [PATCH 08/22] tests: parser: updated the parser tests that caused a
 failure due to the lack of engines section

---
 tests/parser/setup.sby | 2 ++
 tests/parser/stage.sby | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/tests/parser/setup.sby b/tests/parser/setup.sby
index 6ca49e3..9b7e468 100644
--- a/tests/parser/setup.sby
+++ b/tests/parser/setup.sby
@@ -3,6 +3,8 @@ mode bmc
 depth 1
 expect error
 
+[engines]
+smtbmc
 
 [setup]
 enable *
diff --git a/tests/parser/stage.sby b/tests/parser/stage.sby
index b69a186..7048b60 100644
--- a/tests/parser/stage.sby
+++ b/tests/parser/stage.sby
@@ -3,6 +3,8 @@ mode bmc
 depth 1
 expect error
 
+[engines]
+smtbmc
 
 [stage stage_1]
 mode prove

From 987e439967d5894bf7525e6a44db1b6f1d585c7d Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Fri, 29 Jul 2022 10:51:25 -0400
Subject: [PATCH 09/22] tests: parser: added the stages option to the options
 test file

---
 tests/parser/options.sby | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/tests/parser/options.sby b/tests/parser/options.sby
index 666953d..bf6a553 100644
--- a/tests/parser/options.sby
+++ b/tests/parser/options.sby
@@ -2,3 +2,7 @@
 mode bmc
 depth 1
 expect error
+stages foo,bar,nya
+
+[engines]
+smtbmc

From e4a7f624c1483451a9dd331b518ba96a87587767 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Fri, 29 Jul 2022 10:52:49 -0400
Subject: [PATCH 10/22] sby: core: config: fixed the engines section parsing
 where it was not setting the engine mode when parsing the section

---
 sbysrc/sby_core.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index d5de81f..b4c9573 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -301,6 +301,7 @@ class SbyConfig:
                         pass
                         # if entries[1] not in self.engines:
                         #     self.engines[entries[1]] = list()
+                        #     engine_mode = entries[1]
                         # else:
                         #     self.error(f"Already defined engine block for mode '{entries[1]}'")
 

From 2f841e5d55f2c0a0d408b4cee38ee92bb92657ef Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Tue, 2 Aug 2022 08:38:24 -0400
Subject: [PATCH 11/22] sby: core: updated the parsing to match the changes in
 PR #206

---
 sbysrc/sby_core.py | 37 ++++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 15 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index b4c9573..81b0da1 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -290,6 +290,7 @@ class SbyConfig:
                         self.error(f"sby file syntax error: '[options]' section does not accept any arguments. got {args}")
                     continue
 
+                # [engines (MODE)]
                 if section == "engines":
                     mode = "engines"
                     if len(entries) > 2:
@@ -306,30 +307,36 @@ class SbyConfig:
                         #     self.error(f"Already defined engine block for mode '{entries[1]}'")
 
                 # [setup]
-                if entries[0] == "setup":
+                if section == "setup":
                     mode = "setup"
-                    if len(self.setup) != 0 or len(entries) != 1:
-                        self.error(f"sby file syntax error: {line}")
-                    continue
+                    if len(self.setup) != 0:
+                        self.error(f"sby file syntax error: '[setup]' section already defined")
+
+                    if args is not None:
+                        self.error(f"sby file syntax error: '[setup]' section does not accept any arguments. got {args}")
 
                 # [stage <NAME> (PARENTS,...)]
-                if entries[0] == "stage":
+                if section == "stage":
                     mode = "stage"
-                    if len(entries) > 3 or len(entries) < 2:
-                        self.error(f"sby file syntax error: {line}")
 
-                    if len(entries) == 2:
-                        parent = None
+                    if args is None:
+                        self.error(f"sby file syntax error: '[stage]' section expects arguments, got none")
+
+                    section_args = args.split(" ", maxsplit = 1)
+
+
+                    if len(section_args) == 1:
+                        parents = None
                     else:
-                        parent = entries[2].split(',')
+                        parents = list(map(lambda a: a.trim(), section_args[1].split(',')))
 
-                    key = entries[1]
+                    stage_name = section_args[0]
 
-                    if key in self.stage:
-                        self.error(f"stage {key} already defined")
+                    if stage_name in self.stage:
+                        self.error(f"stage {stage_name} already defined")
 
-                    self.stage[key] = {
-                        'parent': parent
+                    self.stage[stage_name] = {
+                        'parents': parents
                     }
 
                     continue

From ad4f506d2a1e4b8354dc2ec43e4e9a8166ab83e8 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 4 Aug 2022 06:32:32 -0400
Subject: [PATCH 12/22] sby: core: fixed up the `engines` section parser

---
 sbysrc/sby_core.py | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 81b0da1..9f4b48b 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -293,18 +293,22 @@ class SbyConfig:
                 # [engines (MODE)]
                 if section == "engines":
                     mode = "engines"
-                    if len(entries) > 2:
-                        self.error(f"sby file syntax error: [engine] sections expects at most 1 argument, got more '{line}'")
 
-                    if len(entries) == 2 and entries[1] not in ("bmc", "prove", "cover", "live"):
-                        self.error(f"sby file syntax error: Expected one of 'bmc, prove, cover, live' not '{entries[1]}'")
-                    elif len(entries) == 2:
-                        pass
-                        # if entries[1] not in self.engines:
-                        #     self.engines[entries[1]] = list()
-                        #     engine_mode = entries[1]
-                        # else:
-                        #     self.error(f"Already defined engine block for mode '{entries[1]}'")
+                    if args is not None:
+                        section_args = args.split()
+
+                        if len(section_args) > 1:
+                            self.error(f"sby file syntax error: '[engine]' sections expects at most 1 argument, got '{len(section_args)}'")
+
+                        if section_args[0] not in ("bmc", "prove", "cover", "live"):
+                            self.error(f"sby file syntax error: Expected one of 'bmc, prove, cover, live' as '[engine]` argument, not '{section_args[0]}'")
+
+                        if section_args[0] in self.engines:
+                            self.error(f"Already defined engine block for mode '{section_args[0]}'")
+                        else:
+                            self.engines[section_args[0]] = list()
+                            engine_mode = section_args[0]
+                    continue
 
                 # [setup]
                 if section == "setup":

From 6c959577f39462e733f8376de1514b38c55a20fe Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 4 Aug 2022 06:56:11 -0400
Subject: [PATCH 13/22] sby: core: cleaned up the `[stage]` section parsing

---
 sbysrc/sby_core.py | 54 +++++++++++++++++++++++++++-------------------
 1 file changed, 32 insertions(+), 22 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 9f4b48b..711e331 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -259,6 +259,7 @@ class SbyConfig:
     def parse_config(self, f):
         mode = None
         engine_mode = None
+        stage_name = None
 
         for line in f:
             raw_line = line
@@ -326,7 +327,7 @@ class SbyConfig:
                     if args is None:
                         self.error(f"sby file syntax error: '[stage]' section expects arguments, got none")
 
-                    section_args = args.split(" ", maxsplit = 1)
+                    section_args = args.strip().split(maxsplit = 1)
 
 
                     if len(section_args) == 1:
@@ -424,31 +425,40 @@ class SbyConfig:
                 continue
 
             if mode == "stage":
-                kvp = line.split()
-                if key is None or key == '':
-                    self.error(f"sby file syntax error: in stage mode but unknown key")
+                _valid_options = (
+                    "mode", "depth", "timeout", "expect", "engine",
+                    "cutpoint", "enable", "disable", "assume", "skip",
+                    "check", "prove", "abstract", "setsel"
+                )
 
-                if len(kvp) == 0:
-                    continue
+                args = line.strip().split(maxsplit = 1)
 
-                if kvp[0] not in ("mode", "depth", "timeout", "expect", "engine",
-                                  "cutpoint", "enable", "disable", "assume", "skip",
-                                  "check", "prove", "abstract", "setsel") or len(kvp) < 2:
-                    self.error(f"sby file syntax error: {line}")
+                if args is None:
+                    self.error(f"sby file syntax error: unknown key in '[stage]' section")
+
+                if len(args) < 2:
+                    self.error(f"sby file syntax error: entry in '[stage]' must have an argument, got {' '.join(args)}")
+
+                if args[0] not in _valid_options:
+                    self.error(f"sby file syntax error: expected on of '{', '.join(_valid_options)}' in '[stage]' section, got '{args[0]}'")
                 else:
-                    stmt = kvp[0]
-                    if stmt == 'setsel':
-                        if len(kvp[1:]) < 2:
-                            self.error(f"sby file syntax error: 'setsel' statement takes 2 arguments, got {len(kvp[1:])}")
-                        elif kvp[1][0] != '@':
-                            self.error(f"sby file syntax error: 'setsel' statement expects an '@' prefixed name as the first parameter, got {line}")
-                        else:
-                            name = kvp[1][1:]
-                            self.stage[key][stmt] = {
-                                'name': name, 'pattern': kvp[2:]
-                            }
+                    opt_key = args[0]
+                    opt_args = args[1].strip().split()
+                    if opt_key == 'setsel':
+
+                        if len(opt_args) != 2:
+                            self.error(f"sby file syntax error: 'setsel' statement in '[stage]' section takes  exactly 2 arguments, got {len(opt_args)}")
+
+                        if opt_args[0][0] != '@':
+                            self.error(f"sby file syntax error: 'setsel' statement in '[stage]' section expects an '@' prefixed name as the first parameter, got {opt_args[0]}")
+
+                        name = opt_args[0][1:]
+                        self.stage[stage_name][opt_key] = {
+                            'name': name, 'pattern': opt_args[2:]
+                        }
+
                     else:
-                        self.stage[key][stmt] = kvp[1:]
+                        self.stage[stage_name][opt_key] = opt_args[1:]
                 continue
 
             if mode == "script":

From 98fdcd7772bad802d5d30563f992ad445926250f Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 4 Aug 2022 07:05:32 -0400
Subject: [PATCH 14/22] sby: core: fixed up the `[setup]` section

---
 sbysrc/sby_core.py | 54 +++++++++++++++++++++++++++++++++++-----------
 1 file changed, 41 insertions(+), 13 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 711e331..ddc342f 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -320,6 +320,8 @@ class SbyConfig:
                     if args is not None:
                         self.error(f"sby file syntax error: '[setup]' section does not accept any arguments. got {args}")
 
+                    continue
+
                 # [stage <NAME> (PARENTS,...)]
                 if section == "stage":
                     mode = "stage"
@@ -404,24 +406,40 @@ class SbyConfig:
                 continue
 
             if mode == "setup":
-                kvp = line.split()
-                if kvp[0] not in ("cutpoint", "disable", "enable", "assume", "define"):
-                    self.error(f"sby file syntax error: found '{kvp[0]}' but expected one of 'cutpoint', 'disable', 'enable', 'assume', or 'define'")
+                _valid_options = (
+                    "cutpoint", "disable", "enable", "assume", "define"
+                )
+
+                args = line.strip().split(maxsplit = 1)
+
+
+                if args is None:
+                    self.error(f"sby file syntax error: unknown key in '[setup]' section")
+
+                if len(args) < 2:
+                    self.error(f"sby file syntax error: entry in '[setup]' must have an argument, got {' '.join(args)}")
+
+                if args[0] not in _valid_options:
+                    self.error(f"sby file syntax error: expected on of '{', '.join(_valid_options)}' in '[setup]' section, got '{args[0]}'")
+
                 else:
-                    stmt = kvp[0]
-                    if stmt == 'define':
+                    opt_key = args[0]
+                    opt_args = args[1].strip().split()
+
+                    if opt_key == 'define':
                         if 'define' not in self.setup:
                             self.setup['define'] = {}
 
-                        if len(kvp[1:]) < 2:
-                            self.error(f"sby file syntax error: 'define' statement takes 2 arguments, got {len(kvp[1:])}")
-                        elif kvp[1][0] != '@':
-                            self.error(f"sby file syntax error: 'define' statement expects an '@' prefixed name as the first parameter, got {line}")
-                        else:
-                            name = kvp[1][1:]
-                            self.setup['define'][name] = kvp[2:]
+                        if len(opt_args) != 2:
+                            self.error(f"sby file syntax error: 'define' statement in '[setup]' section takes  exactly 2 arguments, got {len(opt_args)}")
+
+                        if opt_args[0][0] != '@':
+                            self.error(f"sby file syntax error: 'define' statement in '[setup]' section expects an '@' prefixed name as the first parameter, got {opt_args[0]}")
+
+                        name = opt_args[0][1:]
+                        self.setup['define'][name] =  opt_args[2:]
                     else:
-                        self.setup[stmt] = kvp[1:]
+                        self.setup[opt_key] =  opt_args[1:]
                 continue
 
             if mode == "stage":
@@ -453,11 +471,18 @@ class SbyConfig:
                             self.error(f"sby file syntax error: 'setsel' statement in '[stage]' section expects an '@' prefixed name as the first parameter, got {opt_args[0]}")
 
                         name = opt_args[0][1:]
+
+                        if stage_name not in self.stage:
+                            self.stage[stage_name] = dict()
+
                         self.stage[stage_name][opt_key] = {
                             'name': name, 'pattern': opt_args[2:]
                         }
 
                     else:
+                        if stage_name not in self.stage:
+                            self.stage[stage_name] = dict()
+
                         self.stage[stage_name][opt_key] = opt_args[1:]
                 continue
 
@@ -483,6 +508,9 @@ class SbyConfig:
 
             self.error(f"sby file syntax error: In an incomprehensible mode '{mode}'")
 
+        if len(self.stage.keys()) == 0:
+            self.stage['default'] = { 'enable': '*' }
+
     def error(self, logmessage):
         raise SbyAbort(logmessage)
 

From da56a3c6d175571c51e0005d380169550df6e1a9 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 4 Aug 2022 07:39:00 -0400
Subject: [PATCH 15/22] docs: started working on a rough draft of the docs for
 the new sections and changes to existing sections

---
 docs/source/reference.rst | 58 +++++++++++++++++++++++++++++++++++++++
 tests/parser/options.sby  |  8 ------
 2 files changed, 58 insertions(+), 8 deletions(-)
 delete mode 100644 tests/parser/options.sby

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 710ba7b..4af5e0a 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -178,6 +178,9 @@ options are:
 |                  | ``prove``, | specified number of cycles at the end of the trace.     |
 |                  | ``cover``  | Default: ``0``                                          |
 +------------------+------------+---------------------------------------------------------+
+| ``stage``        | All        | The stages to select to run.                            |
+|                  |            | Default: All                                            |
++------------------+------------+---------------------------------------------------------+
 
 Engines section
 ---------------
@@ -205,6 +208,19 @@ solver options.
 In the 2nd line ``abc`` is the engine, there are no engine options, ``sim3`` is the
 solver, and ``-W 15`` are solver options.
 
+
+The ``[engines]`` section also takes an argument as to what mode that block applies to.
+Meaning you can specify an engine block for a given mode.
+
+Example:
+
+.. code-block:: text
+
+   [engines bmc]
+   btor pono
+   abc sim3
+
+
 The following mode/engine/solver combinations are currently supported:
 
 +-----------+--------------------------+
@@ -391,6 +407,48 @@ Run ``yosys`` in a terminal window and enter ``help`` on the Yosys prompt
 for a command list. Run ``help <command>`` for a detailed description of the
 command, for example ``help prep``.
 
+Setup section
+-------------
+
+The ``[setup]`` section provides a way to add global cutpoints, and enable/disable/assume/define patterns.
+By default properties that are unspecified default to enabled, and a ``disable *`` at the end of the settings
+will set the default to be disabled.
+
+For example:
+
+.. code-block:: text
+
+   [setup]
+   enable *
+
+The following options are available for the ``[setup]`` section:
+
+.. todo::
+
+   Document better
+
++------------------+---------------------------------------------------------+
+|   Option         | Description                                             |
++==================+=========================================================+
+| ``cutpoint``     | Defines a cutpoint pattern.                             |
++------------------+---------------------------------------------------------+
+| ``disable``      | Defines a disable pattern.                              |
++------------------+---------------------------------------------------------+
+| ``enable``       | Defines an enable pattern.                              |
++------------------+---------------------------------------------------------+
+| ``assume``       | Defines an assume pattern.                              |
++------------------+---------------------------------------------------------+
+| ``define``       | Define a value.                                         |
++------------------+---------------------------------------------------------+
+
+
+Stage section
+-------------
+
+.. todo::
+
+   Document
+
 Files section
 -------------
 
diff --git a/tests/parser/options.sby b/tests/parser/options.sby
deleted file mode 100644
index bf6a553..0000000
--- a/tests/parser/options.sby
+++ /dev/null
@@ -1,8 +0,0 @@
-[options]
-mode bmc
-depth 1
-expect error
-stages foo,bar,nya
-
-[engines]
-smtbmc

From 637095a8ecd2014df1b0a998003911fe29349914 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 4 Aug 2022 08:51:35 -0400
Subject: [PATCH 16/22] sby: fixed the sby task execution to accept the new
 engine internal layout

---
 sbysrc/sby_core.py       |  4 ++--
 sbysrc/sby_mode_bmc.py   | 10 ++++++++--
 sbysrc/sby_mode_cover.py |  9 +++++++--
 sbysrc/sby_mode_live.py  |  9 +++++++--
 sbysrc/sby_mode_prove.py |  9 +++++++--
 5 files changed, 31 insertions(+), 10 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index ddc342f..7ea25fc 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -401,8 +401,8 @@ class SbyConfig:
                 continue
 
             if mode == "engines":
-                entries = line.split()
-                self.engines[engine_mode].append(entries)
+                args = line.strip().split()
+                self.engines[engine_mode].append(args)
                 continue
 
             if mode == "setup":
diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index e8f4f71..e9afbc5 100644
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -25,13 +25,19 @@ def run(task):
     task.handle_str_option("aigsmt", "yices")
 
     for engine_idx, engine_section in task.engine_list():
-        engine = engine_section[1][0]
-        engine_name = engine_section[0]
+        if isinstance(engine_section, list):
+            engine = engine_section
+            engine_name = None
+        else:
+            engine = engine_section[1][0]
+            engine_name = engine_section[0]
+
         if engine_name is None:
             engine_name = engine_idx
 
         assert len(engine) > 0
 
+
         task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py
index f918247..f1e6ff5 100644
--- a/sbysrc/sby_mode_cover.py
+++ b/sbysrc/sby_mode_cover.py
@@ -24,8 +24,13 @@ def run(task):
     task.handle_int_option("append", 0)
 
     for engine_idx, engine_section in task.engine_list():
-        engine = engine_section[1][0]
-        engine_name = engine_section[0]
+        if isinstance(engine_section, list):
+            engine = engine_section
+            engine_name = None
+        else:
+            engine = engine_section[1][0]
+            engine_name = engine_section[0]
+
         if engine_name is None:
             engine_name = engine_idx
 
diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py
index d713215..bdc772c 100644
--- a/sbysrc/sby_mode_live.py
+++ b/sbysrc/sby_mode_live.py
@@ -25,8 +25,13 @@ def run(task):
     task.status = "UNKNOWN"
 
     for engine_idx, engine_section in task.engine_list():
-        engine = engine_section[1][0]
-        engine_name = engine_section[0]
+        if isinstance(engine_section, list):
+            engine = engine_section
+            engine_name = None
+        else:
+            engine = engine_section[1][0]
+            engine_name = engine_section[0]
+
         if engine_name is None:
             engine_name = engine_idx
 
diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index c4dcb0d..36f9929 100644
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -32,8 +32,13 @@ def run(task):
     task.induction_procs = list()
 
     for engine_idx, engine_section in task.engine_list():
-        engine = engine_section[1][0]
-        engine_name = engine_section[0]
+        if isinstance(engine_section, list):
+            engine = engine_section
+            engine_name = None
+        else:
+            engine = engine_section[1][0]
+            engine_name = engine_section[0]
+
         if engine_name is None:
             engine_name = engine_idx
 

From 841e0cb797b920067d23918df138c12d8bbfdf58 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 4 Aug 2022 09:41:24 -0400
Subject: [PATCH 17/22] sby: core: Added unsupported messages to the new
 sections

---
 sbysrc/sby_core.py       |  6 ++++--
 tests/parser/engines.sby | 13 -------------
 tests/parser/setup.sby   | 10 ----------
 tests/parser/stage.sby   | 14 --------------
 4 files changed, 4 insertions(+), 39 deletions(-)
 delete mode 100644 tests/parser/engines.sby
 delete mode 100644 tests/parser/setup.sby
 delete mode 100644 tests/parser/stage.sby

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 7ea25fc..a1e42a2 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -291,7 +291,6 @@ class SbyConfig:
                         self.error(f"sby file syntax error: '[options]' section does not accept any arguments. got {args}")
                     continue
 
-                # [engines (MODE)]
                 if section == "engines":
                     mode = "engines"
 
@@ -311,8 +310,9 @@ class SbyConfig:
                             engine_mode = section_args[0]
                     continue
 
-                # [setup]
                 if section == "setup":
+                    self.error(f"sby file syntax error: the '[setup]' section is not yet supported")
+
                     mode = "setup"
                     if len(self.setup) != 0:
                         self.error(f"sby file syntax error: '[setup]' section already defined")
@@ -324,6 +324,8 @@ class SbyConfig:
 
                 # [stage <NAME> (PARENTS,...)]
                 if section == "stage":
+                    self.error(f"sby file syntax error: the '[stage]' section is not yet supported")
+
                     mode = "stage"
 
                     if args is None:
diff --git a/tests/parser/engines.sby b/tests/parser/engines.sby
deleted file mode 100644
index 2277151..0000000
--- a/tests/parser/engines.sby
+++ /dev/null
@@ -1,13 +0,0 @@
-[options]
-mode bmc
-depth 1
-expect error
-
-[engines]
-smtbmc
-
-[engines bmc]
-smtbmc
-
-[engines cover]
-smtbmc
diff --git a/tests/parser/setup.sby b/tests/parser/setup.sby
deleted file mode 100644
index 9b7e468..0000000
--- a/tests/parser/setup.sby
+++ /dev/null
@@ -1,10 +0,0 @@
-[options]
-mode bmc
-depth 1
-expect error
-
-[engines]
-smtbmc
-
-[setup]
-enable *
diff --git a/tests/parser/stage.sby b/tests/parser/stage.sby
deleted file mode 100644
index 7048b60..0000000
--- a/tests/parser/stage.sby
+++ /dev/null
@@ -1,14 +0,0 @@
-[options]
-mode bmc
-depth 1
-expect error
-
-[engines]
-smtbmc
-
-[stage stage_1]
-mode prove
-depth 20
-timeout 60
-expect error
-enable *

From a6c220dd5d73aca3eab0ccc43865510063291232 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Fri, 5 Aug 2022 08:22:55 -0400
Subject: [PATCH 18/22] docs:  Cut out the in-progress docs in preperation for
 a merge

---
 docs/source/reference.rst | 56 ---------------------------------------
 sbysrc/sby_core.py        |  5 ----
 2 files changed, 61 deletions(-)

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 4af5e0a..370001e 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -178,9 +178,6 @@ options are:
 |                  | ``prove``, | specified number of cycles at the end of the trace.     |
 |                  | ``cover``  | Default: ``0``                                          |
 +------------------+------------+---------------------------------------------------------+
-| ``stage``        | All        | The stages to select to run.                            |
-|                  |            | Default: All                                            |
-+------------------+------------+---------------------------------------------------------+
 
 Engines section
 ---------------
@@ -209,18 +206,6 @@ In the 2nd line ``abc`` is the engine, there are no engine options, ``sim3`` is
 solver, and ``-W 15`` are solver options.
 
 
-The ``[engines]`` section also takes an argument as to what mode that block applies to.
-Meaning you can specify an engine block for a given mode.
-
-Example:
-
-.. code-block:: text
-
-   [engines bmc]
-   btor pono
-   abc sim3
-
-
 The following mode/engine/solver combinations are currently supported:
 
 +-----------+--------------------------+
@@ -407,47 +392,6 @@ Run ``yosys`` in a terminal window and enter ``help`` on the Yosys prompt
 for a command list. Run ``help <command>`` for a detailed description of the
 command, for example ``help prep``.
 
-Setup section
--------------
-
-The ``[setup]`` section provides a way to add global cutpoints, and enable/disable/assume/define patterns.
-By default properties that are unspecified default to enabled, and a ``disable *`` at the end of the settings
-will set the default to be disabled.
-
-For example:
-
-.. code-block:: text
-
-   [setup]
-   enable *
-
-The following options are available for the ``[setup]`` section:
-
-.. todo::
-
-   Document better
-
-+------------------+---------------------------------------------------------+
-|   Option         | Description                                             |
-+==================+=========================================================+
-| ``cutpoint``     | Defines a cutpoint pattern.                             |
-+------------------+---------------------------------------------------------+
-| ``disable``      | Defines a disable pattern.                              |
-+------------------+---------------------------------------------------------+
-| ``enable``       | Defines an enable pattern.                              |
-+------------------+---------------------------------------------------------+
-| ``assume``       | Defines an assume pattern.                              |
-+------------------+---------------------------------------------------------+
-| ``define``       | Define a value.                                         |
-+------------------+---------------------------------------------------------+
-
-
-Stage section
--------------
-
-.. todo::
-
-   Document
 
 Files section
 -------------
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index a1e42a2..c94e988 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -945,11 +945,6 @@ class SbyTask(SbyConfig):
         with open(f"{self.workdir}/config.sby", "r") as f:
             self.parse_config(f)
 
-        if len(self.stage) == 0:
-            self.stage['default'] = {
-                'enable', '*'
-            }
-
         self.handle_str_option("mode", None)
 
         if self.opt_mode not in ["bmc", "prove", "cover", "live"]:

From e8b8816143cd7eef51f79d1927c9021de75e3aaa Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Wed, 17 Aug 2022 09:02:13 -0400
Subject: [PATCH 19/22] docs: removed empty line

---
 docs/source/reference.rst | 1 -
 1 file changed, 1 deletion(-)

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 370001e..589f997 100644
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -205,7 +205,6 @@ solver options.
 In the 2nd line ``abc`` is the engine, there are no engine options, ``sim3`` is the
 solver, and ``-W 15`` are solver options.
 
-
 The following mode/engine/solver combinations are currently supported:
 
 +-----------+--------------------------+

From 8f5508142d02a9d373b613225ae37c765fbc886f Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Wed, 17 Aug 2022 09:03:34 -0400
Subject: [PATCH 20/22] sby: core: minor error message cleanups for consistency

---
 sbysrc/sby_core.py | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index c94e988..8c1ebac 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -298,10 +298,10 @@ class SbyConfig:
                         section_args = args.split()
 
                         if len(section_args) > 1:
-                            self.error(f"sby file syntax error: '[engine]' sections expects at most 1 argument, got '{len(section_args)}'")
+                            self.error(f"sby file syntax error: '[engines]' section expects at most 1 argument, got '{' '.join(section_args)}'")
 
                         if section_args[0] not in ("bmc", "prove", "cover", "live"):
-                            self.error(f"sby file syntax error: Expected one of 'bmc, prove, cover, live' as '[engine]` argument, not '{section_args[0]}'")
+                            self.error(f"sby file syntax error: Expected one of 'bmc', 'prove', 'cover', 'live' as '[engines]' argument, got '{section_args[0]}'")
 
                         if section_args[0] in self.engines:
                             self.error(f"Already defined engine block for mode '{section_args[0]}'")
@@ -318,7 +318,7 @@ class SbyConfig:
                         self.error(f"sby file syntax error: '[setup]' section already defined")
 
                     if args is not None:
-                        self.error(f"sby file syntax error: '[setup]' section does not accept any arguments. got {args}")
+                        self.error(f"sby file syntax error: '[setup]' section does not accept any arguments, got '{args}'")
 
                     continue
 
@@ -337,12 +337,12 @@ class SbyConfig:
                     if len(section_args) == 1:
                         parents = None
                     else:
-                        parents = list(map(lambda a: a.trim(), section_args[1].split(',')))
+                        parents = list(map(lambda a: a.strip(), section_args[1].split(',')))
 
                     stage_name = section_args[0]
 
                     if stage_name in self.stage:
-                        self.error(f"stage {stage_name} already defined")
+                        self.error(f"stage '{stage_name}' already defined")
 
                     self.stage[stage_name] = {
                         'parents': parents
@@ -419,10 +419,10 @@ class SbyConfig:
                     self.error(f"sby file syntax error: unknown key in '[setup]' section")
 
                 if len(args) < 2:
-                    self.error(f"sby file syntax error: entry in '[setup]' must have an argument, got {' '.join(args)}")
+                    self.error(f"sby file syntax error: entry in '[setup]' must have an argument, got '{' '.join(args)}'")
 
                 if args[0] not in _valid_options:
-                    self.error(f"sby file syntax error: expected on of '{', '.join(_valid_options)}' in '[setup]' section, got '{args[0]}'")
+                    self.error(f"sby file syntax error: expected one of '{', '.join(_valid_options)}' in '[setup]' section, got '{args[0]}'")
 
                 else:
                     opt_key = args[0]
@@ -433,10 +433,10 @@ class SbyConfig:
                             self.setup['define'] = {}
 
                         if len(opt_args) != 2:
-                            self.error(f"sby file syntax error: 'define' statement in '[setup]' section takes  exactly 2 arguments, got {len(opt_args)}")
+                            self.error(f"sby file syntax error: 'define' statement in '[setup]' section takes  exactly 2 arguments, got '{' '.join(opt_args)}'")
 
                         if opt_args[0][0] != '@':
-                            self.error(f"sby file syntax error: 'define' statement in '[setup]' section expects an '@' prefixed name as the first parameter, got {opt_args[0]}")
+                            self.error(f"sby file syntax error: 'define' statement in '[setup]' section expects an '@' prefixed name as the first parameter, got '{opt_args[0]}'")
 
                         name = opt_args[0][1:]
                         self.setup['define'][name] =  opt_args[2:]
@@ -460,17 +460,17 @@ class SbyConfig:
                     self.error(f"sby file syntax error: entry in '[stage]' must have an argument, got {' '.join(args)}")
 
                 if args[0] not in _valid_options:
-                    self.error(f"sby file syntax error: expected on of '{', '.join(_valid_options)}' in '[stage]' section, got '{args[0]}'")
+                    self.error(f"sby file syntax error: expected one of '{', '.join(map(repr, _valid_options))}' in '[stage]' section, got '{args[0]}'")
                 else:
                     opt_key = args[0]
                     opt_args = args[1].strip().split()
                     if opt_key == 'setsel':
 
                         if len(opt_args) != 2:
-                            self.error(f"sby file syntax error: 'setsel' statement in '[stage]' section takes  exactly 2 arguments, got {len(opt_args)}")
+                            self.error(f"sby file syntax error: 'setsel' statement in '[stage]' section takes  exactly 2 arguments, got '{' '.join(opt_args)}'")
 
                         if opt_args[0][0] != '@':
-                            self.error(f"sby file syntax error: 'setsel' statement in '[stage]' section expects an '@' prefixed name as the first parameter, got {opt_args[0]}")
+                            self.error(f"sby file syntax error: 'setsel' statement in '[stage]' section expects an '@' prefixed name as the first parameter, got '{opt_args[0]}'")
 
                         name = opt_args[0][1:]
 

From 41b4ce5a7e19134d4d82f88b906d0d4d246e7086 Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 18 Aug 2022 05:51:03 -0400
Subject: [PATCH 21/22] sby: fixed issue where engine index would be out of
 range

---
 sbysrc/sby_core.py       | 7 ++++---
 sbysrc/sby_mode_bmc.py   | 3 +--
 sbysrc/sby_mode_cover.py | 4 +---
 sbysrc/sby_mode_live.py  | 3 +--
 sbysrc/sby_mode_prove.py | 3 +--
 5 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 8c1ebac..e4d58a5 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -246,8 +246,7 @@ class SbyAbort(BaseException):
 class SbyConfig:
     def __init__(self):
         self.options = dict()
-        # Define a default case for the engine block
-        self.engines = { None: list() }
+        self.engines = dict()
         self.setup = dict()
         self.stage = dict()
         self.script = list()
@@ -263,7 +262,7 @@ class SbyConfig:
 
         for line in f:
             raw_line = line
-            if mode in ["options", "engines", "files", "autotune"]:
+            if mode in ["options", "engines", "files", "autotune", "setup", "stage"]:
                 line = re.sub(r"\s*(\s#.*)?$", "", line)
                 if line == "" or line[0] == "#":
                     continue
@@ -404,6 +403,8 @@ class SbyConfig:
 
             if mode == "engines":
                 args = line.strip().split()
+                if engine_mode not in self.engines:
+                    self.engines[engine_mode] = list()
                 self.engines[engine_mode].append(args)
                 continue
 
diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py
index e9afbc5..2613efa 100644
--- a/sbysrc/sby_mode_bmc.py
+++ b/sbysrc/sby_mode_bmc.py
@@ -29,14 +29,13 @@ def run(task):
             engine = engine_section
             engine_name = None
         else:
+            assert len(engine_section[1]) > 0
             engine = engine_section[1][0]
             engine_name = engine_section[0]
 
         if engine_name is None:
             engine_name = engine_idx
 
-        assert len(engine) > 0
-
 
         task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py
index f1e6ff5..61d0b07 100644
--- a/sbysrc/sby_mode_cover.py
+++ b/sbysrc/sby_mode_cover.py
@@ -28,15 +28,13 @@ def run(task):
             engine = engine_section
             engine_name = None
         else:
+            assert len(engine_section[1]) > 0
             engine = engine_section[1][0]
             engine_name = engine_section[0]
 
         if engine_name is None:
             engine_name = engine_idx
 
-
-        assert len(engine) > 0
-
         task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py
index bdc772c..c624ec5 100644
--- a/sbysrc/sby_mode_live.py
+++ b/sbysrc/sby_mode_live.py
@@ -29,14 +29,13 @@ def run(task):
             engine = engine_section
             engine_name = None
         else:
+            assert len(engine_section[1]) > 0
             engine = engine_section[1][0]
             engine_name = engine_section[0]
 
         if engine_name is None:
             engine_name = engine_idx
 
-        assert len(engine) > 0
-
         task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py
index 36f9929..f3dc1b7 100644
--- a/sbysrc/sby_mode_prove.py
+++ b/sbysrc/sby_mode_prove.py
@@ -36,14 +36,13 @@ def run(task):
             engine = engine_section
             engine_name = None
         else:
+            assert len(engine_section[1]) > 0
             engine = engine_section[1][0]
             engine_name = engine_section[0]
 
         if engine_name is None:
             engine_name = engine_idx
 
-        assert len(engine) > 0
-
         task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 

From de40cc499f08e517ece48be1ab4f0d3350d0a72a Mon Sep 17 00:00:00 2001
From: Aki Van Ness <aki@yosyshq.com>
Date: Thu, 18 Aug 2022 05:52:38 -0400
Subject: [PATCH 22/22] sby: core: removed invalid None check in setup section

---
 sbysrc/sby_core.py | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index e4d58a5..ad9552c 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -415,10 +415,6 @@ class SbyConfig:
 
                 args = line.strip().split(maxsplit = 1)
 
-
-                if args is None:
-                    self.error(f"sby file syntax error: unknown key in '[setup]' section")
-
                 if len(args) < 2:
                     self.error(f"sby file syntax error: entry in '[setup]' must have an argument, got '{' '.join(args)}'")