Merge pull request #4 from adwait/adwait/svacontext

enh: cleanup SVAGen <-> Jasper interface with SVAContext that maintai…

pycaliper/jginterface/jgoracle.py

@@ -3,6 +3,7 @@
 import os
 
 from . import jasperclient as jgc
+from ..svagen import SVAContext
 
 logger = logging.getLogger(__name__)
 
@@ -30,7 +31,7 @@ def prove(taskcon: str, prop: str) -> ProofResult:
     Returns:
         ProofResult: result of the proof
     """
-    prop_wctx = get_as_asrt_name(taskcon, prop)
+    prop_wctx = get_wctx(taskcon, f"P_{prop}")
     logger.debug(f"Proving property: {prop_wctx}")
     cmd = f"prove -property {{ {prop_wctx} }}"
     res: str = jgc.eval(cmd)
@@ -43,7 +44,7 @@ def is_pass(res: ProofResult) -> bool:
     return res in [ProofResult.SAFE, ProofResult.MAX_TRACE_LENGTH, ProofResult.PROVEN]
 
 
-def get_as_assm_name(taskcon: str, prop: str) -> str:
+def get_wctx(taskcon: str, prop: str) -> str:
     """Get the hierarchical assumption name for a property wire
 
     Args:
@@ -53,20 +54,7 @@ def get_as_assm_name(taskcon: str, prop: str) -> str:
     Returns:
         str: hierarchical assumption name
     """
-    return f"{taskcon}.A_{prop}"
-
-
-def get_as_asrt_name(taskcon: str, prop: str) -> str:
-    """Get the hierarchical assertion name for a property wire
-
-    Args:
-        taskcon (str): proof node name under which the property is defined
-        prop (str): property name
-
-    Returns:
-        str: hierarchical assertion name
-    """
-    return f"{taskcon}.P_{prop}"
+    return f"{taskcon}.{prop}"
 
 
 def disable_assm(taskcon: str, assm: str):
@@ -79,7 +67,7 @@ def disable_assm(taskcon: str, assm: str):
     Returns:
         _type_: result of the JasperGold command
     """
-    assm_wctx = get_as_assm_name(taskcon, assm)
+    assm_wctx = get_wctx(taskcon, f"A_{assm}")
     logger.debug(f"Disabling assumption: {assm_wctx}")
     cmd = f"assume -disable {assm_wctx}"
     res = jgc.eval(cmd)
@@ -97,47 +85,55 @@ def enable_assm(taskcon: str, assm: str):
     Returns:
         _type_: result of the JasperGold command
     """
-    assm_wctx = get_as_assm_name(taskcon, assm)
+    assm_wctx = get_wctx(taskcon, f"A_{assm}")
     logger.debug(f"Enabling assumption: {assm_wctx}")
     cmd = f"assume -enable {assm_wctx}"
     res = jgc.eval(cmd)
     logger.debug(f"Enabling assumption: {assm_wctx} returned {res}")
     return res
 
 
-def set_assm_induction_1t(taskcon: str, symbsim_assms: list[str]):
+def set_assm_induction_1t(taskcon: str, svacon: SVAContext):
     """Enable only 1-trace assumptions (required for 1 trace properties)
 
     Args:
         taskcon (str): proof node name
     """
-    enable_assm(taskcon, "input_inv")
-    enable_assm(taskcon, "state_inv")
-    disable_assm(taskcon, "input")
-    disable_assm(taskcon, "state")
-    for assm in symbsim_assms:
+    for cand in svacon.holes:
+        disable_assm(taskcon, cand)
+    for assm in svacon.assms_2trace:
+        disable_assm(taskcon, assm)
+    for assm in svacon.assms_1trace:
+        enable_assm(taskcon, assm)
+    for assm in svacon.assms_bmc:
         disable_assm(taskcon, assm)
 
-def set_assm_induction_2t(taskcon: str, symbsim_assms: list[str]):
+def set_assm_induction_2t(taskcon: str, svacon: SVAContext):
     """Enable all assumptions required for 2 trace properties
 
     Args:
         taskcon (str): proof node name
     """
-    enable_assm(taskcon, "input")
-    enable_assm(taskcon, "state")
-    enable_assm(taskcon, "input_inv")
-    enable_assm(taskcon, "state_inv")
-    for assm in symbsim_assms:
+    # Disable all holes in the specification
+    for cand in svacon.holes:
+        disable_assm(taskcon, cand)
+    for assm in svacon.assms_2trace:
+        enable_assm(taskcon, assm)
+    for assm in svacon.assms_1trace:
+        disable_assm(taskcon, assm)
+    for assm in svacon.assms_bmc:
         disable_assm(taskcon, assm)
 
-def set_assm_bmc(taskcon: str, symbsim_assms: list[str]):
+def set_assm_bmc(taskcon: str, svacon: SVAContext):
     """Enable all assumptions required for 1 BMC trace properties"""
-    disable_assm(taskcon, "input")
-    disable_assm(taskcon, "state")
-    disable_assm(taskcon, "input_inv")
-    disable_assm(taskcon, "state_inv")
-    for assm in symbsim_assms:
+    # Disable all holes
+    for cand in svacon.holes:
+        disable_assm(taskcon, cand)
+    for assm in svacon.assms_2trace:
+        disable_assm(taskcon, assm)
+    for assm in svacon.assms_1trace:
+        disable_assm(taskcon, assm)
+    for assm in svacon.assms_bmc:
         enable_assm(taskcon, assm)
 
 

pycaliper/propns.py

@@ -0,0 +1,25 @@
+"""
+    Namespace for properties
+"""
+
+# Properties for top module
+TOP_INPUT_2T_PROP = "input"
+TOP_STATE_2T_PROP = "state"
+TOP_OUTPUT_2T_PROP = "output"
+
+TOP_INPUT_1T_PROP = "input_inv"
+TOP_STATE_1T_PROP = "state_inv"
+TOP_OUTPUT_1T_PROP = "output_inv"
+
+STEP_PROP = "step"
+def TOP_STEP_PROP(k: int) -> str:
+    """Get the property name for a given step"""
+    return f"{STEP_PROP}_{k}"
+
+def get_as_assm(prop: str) -> str:
+    """Get the assumption name for a given property"""
+    return f"A_{prop}"
+
+def get_as_prop(prop: str) -> str:
+    """Get the assertion name for a given property"""
+    return f"P_{prop}"

pycaliper/pycmanager.py

@@ -2,7 +2,6 @@
 import sys
 import logging
 import random
-from dataclasses import dataclass
 from enum import Enum
 
 import tempfile
@@ -41,8 +40,7 @@ class PYCArgs(BaseModel):
     bmc : bool = False
 
 
-@dataclass
-class PYConfig:
+class PYConfig(BaseModel):
     """PyCaliper configuration class"""
 
     # Is this a mock run (without Jasper access)?

pycaliper/svagen.py

@@ -4,40 +4,30 @@
 
 import sys
 import logging
-from dataclasses import dataclass
+from pydantic import BaseModel
 
 from .per import Module, Eq, Path, Context, PER, Inv, PERHole
+from .propns import *
 
 logger = logging.getLogger(__name__)
 
 
+# Internal signals
 COUNTER = "_pycinternal__counter"
-STEP = "_pycinternal__step"
+STEP_SIGNAL = "_pycinternal__step"
 def step_signal(k: int):
-    return f"{STEP}_{k}"
+    return f"{STEP_SIGNAL}_{k}"
 
-def step_property(k: int):
-    return f"step_{k}"
+# def step_property(k: int):
+#     return f"step_{k}"
 
+# Internal wire names
 def eq_sva(s: str):
     return f"eq_{s}"
 
 def condeq_sva(s: str):
     return f"condeq_{s}"
 
-TOP_INPUT_ASSUME_2T = "A_input"
-TOP_STATE_ASSUME_2T = "A_state"
-TOP_OUTPUT_ASSERT_2T = "P_output"
-
-TOP_INPUT_ASSUME_1T = "A_input_inv"
-TOP_STATE_ASSUME_1T = "A_state_inv"
-TOP_OUTPUT_ASSERT_1T = "P_output_inv"
-
-def TOP_STEP_ASSUME(k: int):
-    return f"A_step_{k}"
-def TOP_STEP_ASSERT(k: int):
-    return f"P_step_{k}"
-
 def per_sva(mod: Module, ctx: Context):
     if ctx == Context.INPUT:
         return f"{mod.get_hier_path('_')}_input"
@@ -62,8 +52,7 @@ def inv_sva(mod: Module, ctx: Context):
         sys.exit(1)
 
 
-@dataclass
-class ModuleSpec:
+class ModuleSpec(BaseModel):
     # Module path
     path: Path
     input_spec_decl: str
@@ -77,15 +66,23 @@ class ModuleSpec:
     output_inv_spec_decl_single: str
 
 
+class SVAContext(BaseModel):
+    holes: list[str] = []
+    assms_2trace: list[str] = []
+    asrts_2trace: list[str] = []
+    assms_1trace: list[str] = []
+    asrts_1trace: list[str] = []
+    assms_bmc: list[str] = []
+    asrts_bmc: list[str] = []
+
 class SVAGen:
     def __init__(self, topmod: Module) -> None:
         self.topmod = topmod
         self.specs: dict[Path, ModuleSpec] = {}
 
         self.holes: dict[str, PERHole] = {}
 
-        self.symbsim_assms = []
-        self.symbsim_asrts = []
+        self.property_context = SVAContext()
 
     def _generate_decls_for_per(self, per: PER):
         declbase = per.logic.get_hier_path_nonindex()
@@ -202,16 +199,16 @@ def _generate_decls(self, mod: Module, a: str = "a", b: str = "b"):
         )
 
         self.specs[mod.path] = ModuleSpec(
-            mod.path,
-            input_decl,
-            state_decl,
-            output_decl,
-            input_inv_decl_comp,
-            state_inv_decl_comp,
-            output_inv_decl_comp,
-            input_inv_decl_single,
-            state_inv_decl_single,
-            output_inv_decl_single,
+            path=mod.path,
+            input_spec_decl=input_decl,
+            state_spec_decl=state_decl,
+            output_spec_decl=output_decl,
+            input_inv_spec_decl_comp=input_inv_decl_comp,
+            state_inv_spec_decl_comp=state_inv_decl_comp,
+            output_inv_spec_decl_comp=output_inv_decl_comp,
+            input_inv_spec_decl_single=input_inv_decl_single,
+            state_inv_spec_decl_single=state_inv_decl_single,
+            output_inv_spec_decl_single=output_inv_decl_single,
         )
 
         return (decls, assigns)
@@ -229,44 +226,53 @@ def generate_decls(self, a: str = "a", b: str = "b"):
         output_props_2t = f"{per_sva(self.topmod, Context.OUTPUT)} && {output_props_1t}"
 
         properties.append(
-            f"{TOP_INPUT_ASSUME_1T} : assume property\n" + f"\t({input_props_1t});"
+            f"{get_as_assm(TOP_INPUT_1T_PROP)} : assume property\n" + f"\t({input_props_1t});"
         )
+        self.property_context.assms_1trace.append(TOP_INPUT_1T_PROP)
         properties.append(
-            f"{TOP_STATE_ASSUME_1T} : assume property\n"
-            + f"\t(!({STEP}) |-> ({state_props_1t}));"
+            f"{get_as_assm(TOP_STATE_1T_PROP)} : assume property\n"
+            + f"\t(!({STEP_SIGNAL}) |-> ({state_props_1t}));"
         )
+        self.property_context.assms_1trace.append(TOP_STATE_1T_PROP)
         properties.append(
-            f"{TOP_OUTPUT_ASSERT_1T} : assert property\n"
-            + f"\t({STEP} |-> ({state_props_1t} && {output_props_1t}));"
+            f"{get_as_prop(TOP_OUTPUT_1T_PROP)} : assert property\n"
+            + f"\t({STEP_SIGNAL} |-> ({state_props_1t} && {output_props_1t}));"
         )
+        self.property_context.asrts_1trace.append(TOP_INPUT_1T_PROP)
 
         properties.append(
-            f"{TOP_INPUT_ASSUME_2T} : assume property\n" + f"\t({input_props_2t});"
+            f"{get_as_assm(TOP_INPUT_2T_PROP)} : assume property\n" + f"\t({input_props_2t});"
         )
+        self.property_context.assms_2trace.append(TOP_INPUT_2T_PROP)
         properties.append(
-            f"{TOP_STATE_ASSUME_2T} : assume property\n"
-            + f"\t(!({STEP}) |-> ({state_props_2t}));"
+            f"{get_as_assm(TOP_STATE_2T_PROP)} : assume property\n"
+            + f"\t(!({STEP_SIGNAL}) |-> ({state_props_2t}));"
         )
+        self.property_context.assms_2trace.append(TOP_STATE_2T_PROP)
         properties.append(
-            f"{TOP_OUTPUT_ASSERT_2T} : assert property\n"
-            + f"\t({STEP} |-> ({state_props_2t} && {output_props_2t}));"
+            f"{get_as_prop(TOP_OUTPUT_2T_PROP)} : assert property\n"
+            + f"\t({STEP_SIGNAL} |-> ({state_props_2t} && {output_props_2t}));"
         )
+        self.property_context.asrts_2trace.append(TOP_OUTPUT_2T_PROP)
 
         for hole in self.topmod._perholes:
             if hole.active:
                 if isinstance(hole.per, Eq):
                     assm_prop = (
                         f"A_{eq_sva(hole.per.logic.get_hier_path_flatindex())} : assume property\n"
-                        + f"\t(!({STEP}) |-> {eq_sva(hole.per.logic.get_hier_path('_'))});"
+                        + f"\t(!({STEP_SIGNAL}) |-> {eq_sva(hole.per.logic.get_hier_path('_'))});"
                     )
                     asrt_prop = (
                         f"P_{eq_sva(hole.per.logic.get_hier_path_flatindex())} : assert property\n"
-                        + f"\t(({STEP}) |-> {eq_sva(hole.per.logic.get_hier_path('_'))});"
+                        + f"\t(({STEP_SIGNAL}) |-> {eq_sva(hole.per.logic.get_hier_path('_'))});"
                     )
                     self.holes[
                         eq_sva(hole.per.logic.get_hier_path_flatindex())
                     ] = hole.per.logic
                     properties.extend([assm_prop, asrt_prop])
+                    self.property_context.holes.append(
+                        f"{eq_sva(hole.per.logic.get_hier_path_flatindex())}"
+                    )
 
         return properties, self._generate_decls(self.topmod, a, b)
 
@@ -289,15 +295,15 @@ def generate_step_decls(self, k: int, a: str = "a") -> list[str]:
             assert_spec = "(\n\t" + " && \n\t".join(asserts + ["1'b1"]) + ")"
 
             properties.append(
-                f"{TOP_STEP_ASSUME(i)} : assume property\n"
+                f"{get_as_assm(TOP_STEP_PROP(i))} : assume property\n"
                 + f"\t({step_signal(i)} |-> {assume_spec});"
             )
+            self.property_context.assms_bmc.append(TOP_STEP_PROP(i))
             properties.append(
-                f"{TOP_STEP_ASSERT(i)} : assert property\n"
+                f"{get_as_prop(TOP_STEP_PROP(i))} : assert property\n"
                 + f"\t({step_signal(i)} |-> {assert_spec});"
             )
-            self.symbsim_asrts.append(step_property(i))
-            self.symbsim_assms.append(step_property(i))
+            self.property_context.asrts_bmc.append(TOP_STEP_PROP(i))
 
         return properties
 
@@ -316,7 +322,7 @@ def counter_step(self, k: int):
 \t        end
 \t    end
 \tend
-\tlogic {STEP} = ({COUNTER} == {counter_width}'d{k});
+\tlogic {STEP_SIGNAL} = ({COUNTER} == {counter_width}'d{k});
 """
         for i in range(k):
             vlog += f"\tlogic {step_signal(i)} = ({COUNTER} == {counter_width}'d{i});\n"

pycaliper/synth/persynthesis.py

@@ -176,9 +176,7 @@ def synthesize(self, topmod: Module) -> Module:
         loadscript(self.psc.script)
 
         # Enable and disable the right assumptions
-        for cand in self.candidates:
-            disable_assm(self.psc.context, cand)
-        set_assm_induction_2t(self.psc.context, self.psc.k)
+        set_assm_induction_2t(self.psc.context, self.svagen.property_context)
 
         invs = self._synthesize()