sby: core: fixed the setup script generation and ensured the model for the setup was implemented

sbysrc/sby_core.py

@@ -548,25 +548,29 @@ class SbyConfig:
 
     def gen_setup_script(self):
         script = '# Autogenerated by SBY stage setup\n'
-        script += 'select *'
+        script += 'read_ilang design.il\n'
+        script += 'select *\n'
 
         def cutpoint(v):
-            return f"cutpoint {v}"
+            return f"cutpoint {v}\n"
 
         def disable(v):
-            return f"select -del {v}"
+            return f"select -del {v}\n"
 
         def enable(v):
-            return f"select -add {v}"
+            return f"select -add {v}\n"
 
         def assume(v):
-            return f"chformal -assert2assume {v}"
+            return f"chformal -assert2assume {v}\n"
 
         def define(v):
-            return f"select -set {v}"
+            defines = str()
+            for defn in v:
+                defines += f"select -set {v}\n"
+            return defines
 
         def invoke(v):
-            return f"{v}"
+            return f"{v}\n"
 
         for k, v in self.setup.items():
             script += {
@@ -576,11 +580,12 @@ class SbyConfig:
                 'assume': assume(v),
                 'define': define(v),
                 'invoke': invoke(v)
-            }.get(k, '') + '\n'
+            }.get(k, '')
 
         script += 'select -set _setup %\n'
         script += 'select @_setup %n\n'
         script += 'chformal -assert -remove %\n'
+        script += 'write_ilang design_setup.il\n'
         return script
 
 
@@ -1015,9 +1020,14 @@ class SbyTask(SbyConfig):
             os.makedirs(f"{self.workdir}/model")
 
         if model_name == "prep":
+            has_setup = len(self.setup) > 0
+
             with open(f"""{self.workdir}/model/design_prep.ys""", "w") as f:
                 print(f"# running in {self.workdir}/model/", file=f)
-                print(f"""read_ilang design.il""", file=f)
+                if has_setup:
+                    print(f"""read_ilang design_setup.il""", file=f)
+                else:
+                    print(f"""read_ilang design.il""", file=f)
                 print("scc -select; simplemap; select -clear", file=f)
                 print("memory_nordff", file=f)
                 if self.opt_multiclock:
@@ -1045,7 +1055,7 @@ class SbyTask(SbyConfig):
             proc = SbyProc(
                 self,
                 model_name,
-                self.model("base"),
+                self.model("setup" if has_setup else "base"),
                 "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)
             )
             proc.checkretcode = True
@@ -1195,6 +1205,19 @@ class SbyTask(SbyConfig):
 
             return [proc]
 
+        if model_name == "setup":
+            with open(f"{self.workdir}/model/design_setup.ys", "w") as f:
+                f.write(self.gen_setup_script())
+
+            proc = SbyProc(
+                self,
+                "setup",
+                self.model("base"),
+                f"""cd {self.workdir}/model; {self.exe_paths["yosys"]} -ql design_setup.log design_setup.ys"""
+            )
+
+            return [proc]
+
         self.error(f"Invalid model name: {model_name}")
 
     def model(self, model_name):