From 814b34d02913122802ea5680e9fe9ac645c21af3 Mon Sep 17 00:00:00 2001 From: Adwait Godbole Date: Mon, 14 Oct 2024 18:38:30 -0700 Subject: [PATCH 1/8] feat(BMC): add BMC verification feature - uses the simstep function to declare BMC assumptions and assertions - unrolls model upto a bound Signed-off-by: Adwait Godbole --- pycaliper/jginterface/jgoracle.py | 27 ++++++++-- pycaliper/per/per.py | 54 +++++++++++++++++++ pycaliper/pycmanager.py | 45 ++++++++++++---- pycaliper/svagen.py | 87 ++++++++++++++++++++++--------- pycaliper/synth/persynthesis.py | 8 +-- pycaliper/verif/jgverifier.py | 52 +++++++++++++++--- pycmain.py | 32 +++++++++--- 7 files changed, 248 insertions(+), 57 deletions(-) diff --git a/pycaliper/jginterface/jgoracle.py b/pycaliper/jginterface/jgoracle.py index 414786e..096433c 100644 --- a/pycaliper/jginterface/jgoracle.py +++ b/pycaliper/jginterface/jgoracle.py @@ -105,7 +105,7 @@ def enable_assm(taskcon: str, assm: str): return res -def enable_assm_1t(taskcon: str): +def set_assm_induction_1t(taskcon: str, k: int): """Enable only 1-trace assumptions (required for 1 trace properties) Args: @@ -115,9 +115,10 @@ def enable_assm_1t(taskcon: str): enable_assm(taskcon, "state_inv") disable_assm(taskcon, "input") disable_assm(taskcon, "state") + for i in range(k): + disable_assm(taskcon, f"step_{i}") - -def enable_assm_2t(taskcon: str): +def set_assm_induction_2t(taskcon: str, k: int): """Enable all assumptions required for 2 trace properties Args: @@ -127,15 +128,31 @@ def enable_assm_2t(taskcon: str): enable_assm(taskcon, "state") enable_assm(taskcon, "input_inv") enable_assm(taskcon, "state_inv") + for i in range(k): + disable_assm(taskcon, f"step_{i}") + +def set_assm_bmc(taskcon: str, k: int): + """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 i in range(k): + enable_assm(taskcon, f"step_{i}") -def prove_out_1t(taskcon): +def prove_out_induction_1t(taskcon) -> ProofResult: return prove(taskcon, "output_inv") -def prove_out_2t(taskcon): +def prove_out_induction_2t(taskcon) -> ProofResult: return prove(taskcon, "output") +def prove_out_bmc(taskcon, k: int) -> list[ProofResult]: + results = [] + for i in range(k): + results.append(prove(taskcon, f"step_{i}")) + return results def loadscript(script): # Get pwd diff --git a/pycaliper/per/per.py b/pycaliper/per/per.py index 0d3d456..a59042b 100644 --- a/pycaliper/per/per.py +++ b/pycaliper/per/per.py @@ -607,6 +607,7 @@ class Context(Enum): INPUT = 0 STATE = 1 OUTPUT = 2 + UNROLL = 3 class Hole: @@ -660,6 +661,26 @@ def _lambda(per: PER): return _lambda +class SimulationStep: + + def __init__(self) -> None: + self._pycinternal__assume: list[Expr] = [] + self._pycinternal__assert: list[Expr] = [] + def _assume(self, expr: Expr): + self._pycinternal__assume.append(expr) + def _assert(self, expr: Expr): + self._pycinternal__assert.append(expr) + + +def unroll(b: int): + def unroll_decorator(func): + def wrapper(self: Module, *args): + for i in range(b): + self._pycinternal__simstep = SimulationStep() + func(self, i) + self._pycinternal__simsteps.append(copy.deepcopy(self._pycinternal__simstep)) + return wrapper + return unroll_decorator class Module: """Module class for specifications related to a SV HW module""" @@ -691,6 +712,9 @@ def __init__(self, name="", **kwargs) -> None: self._pycinternal__input_invs: list[Inv] = [] self._pycinternal__state_invs: list[Inv] = [] self._pycinternal__output_invs: list[Inv] = [] + # Non-invariant properties + self._pycinternal__simsteps: list[SimulationStep] = [] + self._pycinternal__simstep : SimulationStep = SimulationStep() # PER holes self._perholes: list[PERHole] = [] # CtrAlign holes @@ -706,6 +730,9 @@ def state(self) -> None: def output(self) -> None: pass + def simstep(self, i: int = 0) -> None: + pass + def eq(self, *elems: TypedElem) -> None: """Create an relational equality invariant""" eqs = [] @@ -820,6 +847,29 @@ def _inv(self, expr: Expr, ctx: Context) -> None: else: self._pycinternal__output_invs.append(Inv(expr)) + def pycassert(self, expr: Expr) -> None: + """Add an assertion to the current context. + + Args: + expr (Expr): the assertion expression. + """ + if self._context == Context.UNROLL: + self._pycinternal__simstep._assert(expr) + else: + logger.warning("pycassert can only be used in the unroll context, skipping.") + + def pycassume(self, expr: Expr) -> None: + """Add an assumption to the current context. + + Args: + expr (Expr): the assumption expression. + """ + if self._context == Context.UNROLL: + self._pycinternal__simstep._assume(expr) + else: + logger.warning("pycassume can only be used in the unroll context, skipping.") + + def instantiate(self, path: Path = Path([])) -> "Module": """Instantiate the current Module. @@ -872,6 +922,9 @@ def instantiate(self, path: Path = Path([])) -> "Module": self.state() self._context = Context.OUTPUT self.output() + # Run through simulation steps + self._context = Context.UNROLL + self.simstep() self._instantiated = True return self @@ -903,6 +956,7 @@ def sprint(self): s += f"\t{i.per} ({i.ctx})\n" return s + def get_repr(self, reprs): # Find all submodules and structs that need to be defined reprs[self.__class__.__name__] = repr(self) diff --git a/pycaliper/pycmanager.py b/pycaliper/pycmanager.py index c40a819..48453aa 100644 --- a/pycaliper/pycmanager.py +++ b/pycaliper/pycmanager.py @@ -24,9 +24,10 @@ class PYCTask(Enum): SVAGEN = 0 VERIF1T = 1 VERIF2T = 2 - CTRLSYNTH = 3 - PERSYNTH = 4 - FULLSYNTH = 5 + VERIFBMC = 3 + CTRLSYNTH = 4 + PERSYNTH = 5 + FULLSYNTH = 6 @dataclass @@ -181,7 +182,8 @@ def save(self): def create_module(specc, args): - specmod = specc["pycspec"] + """Dynamically import the spec module and create an instance of it.""" + specmod : str = specc["pycspec"] params = specc.get("params", {}) parsed_conf = {} @@ -191,16 +193,40 @@ def create_module(specc, args): params.update(parsed_conf) - mod = importlib.import_module(f"specs.{specmod}") - return getattr(mod, specmod)(**params) + if '/' in specmod: + # Split the module name into the module name and the parent package + module_path, module_name = specmod.rsplit('/', 1) + + # Check if the path exists + if not os.path.isdir(module_path): + logger.error(f"Path '{module_path}' does not exist.") + exit(1) + # Add the module path to sys.path + sys.path.append(module_path) + + try: + # Import the module using importlib + module = importlib.import_module(module_name) + logger.debug(f"Successfully imported module: {module_name} from {module_path}") + return getattr(module, module_name)(**params) + except ImportError as e: + logger.error(f"Error importing module {module_name} from {module_path}: {e}") + return None + finally: + # Clean up: remove the path from sys.path to avoid potential side effects + sys.path.remove(module_path) + + else: + mod = importlib.import_module(f"specs.{specmod}") + return getattr(mod, specmod)(**params) -def mock_or_connect(pyconfig: PYConfig): +def mock_or_connect(pyconfig: PYConfig, port: int) -> bool: if pyconfig.mock: logger.info("Running in mock mode.") return False else: - jgc.connect_tcp("localhost", 8080) + jgc.connect_tcp("localhost", port) setjwd(pyconfig.jdir) return True @@ -252,8 +278,9 @@ def start(task: PYCTask, args) -> tuple[PYConfig, PYCManager, Module]: tmgr = PYCManager(pyconfig) module = create_module(config.get("spec"), args) + assert module is not None, f"Module {config.get('spec')['pycspec']} not found." - is_connected = mock_or_connect(pyconfig) + is_connected = mock_or_connect(pyconfig, args.port) match task: case PYCTask.VERIF1T | PYCTask.VERIF2T | PYCTask.PERSYNTH | PYCTask.CTRLSYNTH: diff --git a/pycaliper/svagen.py b/pycaliper/svagen.py index 454b8df..a5d516d 100644 --- a/pycaliper/svagen.py +++ b/pycaliper/svagen.py @@ -11,14 +11,17 @@ logger = logging.getLogger(__name__) +COUNTER = "_pycinternal__counter" +STEP = "_pycinternal__step" +def step(k: int): + return f"{STEP}_{k}" + 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" @@ -27,6 +30,10 @@ def condeq_sva(s: str): 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: @@ -203,8 +210,7 @@ def _generate_decls(self, mod: Module, a: str = "a", b: str = "b"): return (decls, assigns) - def generate_decls(self, check_pred: str, a: str = "a", b: str = "b"): - self.topmod.instantiate() + def generate_decls(self, a: str = "a", b: str = "b"): properties = [] @@ -221,11 +227,11 @@ def generate_decls(self, check_pred: str, a: str = "a", b: str = "b"): ) properties.append( f"{TOP_STATE_ASSUME_1T} : assume property\n" - + f"\t(!({check_pred}) |-> ({state_props_1t}));" + + f"\t(!({STEP}) |-> ({state_props_1t}));" ) properties.append( f"{TOP_OUTPUT_ASSERT_1T} : assert property\n" - + f"\t({check_pred} |-> ({state_props_1t} && {output_props_1t}));" + + f"\t({STEP} |-> ({state_props_1t} && {output_props_1t}));" ) properties.append( @@ -233,11 +239,11 @@ def generate_decls(self, check_pred: str, a: str = "a", b: str = "b"): ) properties.append( f"{TOP_STATE_ASSUME_2T} : assume property\n" - + f"\t(!({check_pred}) |-> ({state_props_2t}));" + + f"\t(!({STEP}) |-> ({state_props_2t}));" ) properties.append( f"{TOP_OUTPUT_ASSERT_2T} : assert property\n" - + f"\t({check_pred} |-> ({state_props_2t} && {output_props_2t}));" + + f"\t({STEP} |-> ({state_props_2t} && {output_props_2t}));" ) for hole in self.topmod._perholes: @@ -245,11 +251,11 @@ def generate_decls(self, check_pred: str, a: str = "a", b: str = "b"): if isinstance(hole.per, Eq): assm_prop = ( f"A_{eq_sva(hole.per.logic.get_hier_path_flatindex())} : assume property\n" - + f"\t(!({check_pred}) |-> {eq_sva(hole.per.logic.get_hier_path('_'))});" + + f"\t(!({STEP}) |-> {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(({check_pred}) |-> {eq_sva(hole.per.logic.get_hier_path('_'))});" + + f"\t(({STEP}) |-> {eq_sva(hole.per.logic.get_hier_path('_'))});" ) self.holes[ eq_sva(hole.per.logic.get_hier_path_flatindex()) @@ -258,31 +264,64 @@ def generate_decls(self, check_pred: str, a: str = "a", b: str = "b"): return properties, self._generate_decls(self.topmod, a, b) + def generate_step_decls(self, k: int, a: str = "a") -> list[str]: + """ + Generate properties for each step in the simulation + + Args: + k (int): Number of steps + a (str, optional): Name of the first trace. Defaults to "a". + + Returns: + list[str]: List of properties for each step + """ + properties = [] + for i in range(min(k, len(self.topmod._pycinternal__simsteps))): + assumes = [expr.get_sva(a) for expr in self.topmod._pycinternal__simsteps[i]._pycinternal__assume] + assume_spec = "(\n\t" + " && \n\t".join(assumes + ["1'b1"]) + ")" + asserts = [expr.get_sva(a) for expr in self.topmod._pycinternal__simsteps[i]._pycinternal__assert] + assert_spec = "(\n\t" + " && \n\t".join(asserts + ["1'b1"]) + ")" + + properties.append( + f"{TOP_STEP_ASSUME(i)} : assume property\n" + + f"\t({step(i)} |-> {assume_spec});" + ) + properties.append( + f"{TOP_STEP_ASSERT(i)} : assert property\n" + + f"\t({step(i)} |-> {assert_spec});" + ) + + return properties + def counter_step(self, k: int): # Create a counter with k steps counter_width = len(bin(k)) - 2 vtype = f"logic [{counter_width-1}:0]" if counter_width > 1 else "logic" vlog = f""" - {vtype} counter; - always @(posedge clk) begin - if (fvreset) begin - counter <= 0; - end else begin - if (counter < {counter_width}'d{k}) begin - counter <= (counter + {counter_width}'b1); - end - end - end - logic step = (counter == {counter_width}'d{k}); +\t{vtype} {COUNTER}; +\talways @(posedge clk) begin +\t if (fvreset) begin +\t {COUNTER} <= 0; +\t end else begin +\t if ({COUNTER} < {counter_width}'d{k}) begin +\t {COUNTER} <= ({COUNTER} + {counter_width}'b1); +\t end +\t end +\tend +\tlogic {STEP} = ({COUNTER} == {counter_width}'d{k}); """ + for i in range(k): + vlog += f"\tlogic {step(i)} = ({COUNTER} == {counter_width}'d{i});\n" return vlog + def create_pyc_specfile(self, k: int, a="a", b="b", filename="temp.pyc.sv"): vlog = self.counter_step(k) - check_pred = f"step" - properties, all_decls = self.generate_decls(check_pred, a, b) + self.topmod.instantiate() + properties, all_decls = self.generate_decls(a, b) + properties.extend(self.generate_step_decls(k, a)) with open(filename, "w") as f: f.write(vlog + "\n") @@ -313,4 +352,4 @@ def create_pyc_specfile(self, k: int, a="a", b="b", filename="temp.pyc.sv"): f.write("\n\n".join(properties)) f.write("\n") - logger.debug(f"Generated spec file: {filename}") + logger.info(f"Generated spec file: {filename}") diff --git a/pycaliper/synth/persynthesis.py b/pycaliper/synth/persynthesis.py index 4bbd87b..3950d18 100644 --- a/pycaliper/synth/persynthesis.py +++ b/pycaliper/synth/persynthesis.py @@ -11,8 +11,8 @@ from pycaliper.svagen import SVAGen from pycaliper.jginterface.jgoracle import ( prove, - prove_out_2t, - enable_assm_2t, + prove_out_induction_2t, + set_assm_induction_2t, is_pass, enable_assm, disable_assm, @@ -128,7 +128,7 @@ def _backtrack(self): def safe(self): if not self.synstate.checked: self.synstate.checked = True - return is_pass(prove_out_2t(self.psc.context)) + return is_pass(prove_out_induction_2t(self.psc.context)) return False def _synthesize(self): @@ -178,7 +178,7 @@ def synthesize(self, topmod: Module) -> Module: # Enable and disable the right assumptions for cand in self.candidates: disable_assm(self.psc.context, cand) - enable_assm_2t(self.psc.context) + set_assm_induction_2t(self.psc.context, self.psc.k) invs = self._synthesize() diff --git a/pycaliper/verif/jgverifier.py b/pycaliper/verif/jgverifier.py index 950d543..c98425c 100644 --- a/pycaliper/verif/jgverifier.py +++ b/pycaliper/verif/jgverifier.py @@ -4,13 +4,15 @@ from .. import svagen from ..jginterface.jgoracle import ( - prove_out_1t, - prove_out_2t, + prove_out_induction_1t, + prove_out_induction_2t, + prove_out_bmc, loadscript, is_pass, disable_assm, - enable_assm_1t, - enable_assm_2t, + set_assm_induction_1t, + set_assm_induction_2t, + set_assm_bmc ) from .invverifier import InvVerifier @@ -44,9 +46,9 @@ def verify(self, module) -> bool: for cand in self.candidates: disable_assm(self.psc.context, cand) # Enable the assumptions for 1 trace verification - enable_assm_1t(self.psc.context) + set_assm_induction_1t(self.psc.context, self.psc.k) - res = is_pass(prove_out_1t(self.psc.context)) + res = is_pass(prove_out_induction_1t(self.psc.context)) res_str = "SAFE" if res else "UNSAFE" logger.info(f"One trace verification result: {res_str}") return res @@ -77,9 +79,43 @@ def verify(self, module): for cand in self.candidates: disable_assm(self.psc.context, cand) # Enable the assumptions for 2 trace verification - enable_assm_2t(self.psc.context) + set_assm_induction_2t(self.psc.context, self.psc.k) - res = is_pass(prove_out_2t(self.psc.context)) + res = is_pass(prove_out_induction_2t(self.psc.context)) res_str = "SAFE" if res else "UNSAFE" logger.info(f"Two trace verification result: {res_str}") return res + +class JGVerifier1TraceBMC(InvVerifier): + """One trace property verifier with BMC""" + + def __init__(self, pyconfig: PYConfig) -> None: + super().__init__(pyconfig) + self.svagen = None + + def verify(self, module): + """Verify one trace properties for the given module + + Args: + module (Module): Module to verify + + Returns: + bool: True if the module is safe, False otherwise + """ + + self.svagen = svagen.SVAGen(module) + self.svagen.create_pyc_specfile(filename=self.psc.pycfile, k=self.psc.k) + self.candidates = self.svagen.holes + + loadscript(self.psc.script) + # Disable all holes in the specification + for cand in self.candidates: + disable_assm(self.psc.context, cand) + # Enable the assumptions for 1 trace verification + set_assm_bmc(self.psc.context, self.psc.k) + + results = [is_pass(r) for r in prove_out_bmc(self.psc.context, self.psc.k)] + results_str = '\n\t'.join( + [f"Step {i}: SAFE" if res else f"Step {i}: UNSAFE" for (i, res) in enumerate(results)]) + logger.info(f"One trace verification result:\n\t{results_str}") + return results diff --git a/pycmain.py b/pycmain.py index 7d31e36..1a3c634 100644 --- a/pycmain.py +++ b/pycmain.py @@ -3,7 +3,7 @@ import json import logging -from pycaliper.verif.jgverifier import JGVerifier1Trace, JGVerifier2Trace +from pycaliper.verif.jgverifier import JGVerifier1Trace, JGVerifier2Trace, JGVerifier1TraceBMC from pycaliper.synth.persynthesis import PERSynthesizer from pycaliper.svagen import SVAGen from pycaliper.synth.alignsynthesis import AlignSynthesizer @@ -25,13 +25,19 @@ def verif_main(args): - - if args.onetrace: - pconfig, tmgr, module = start(PYCTask.VERIF1T, args) - verifier = JGVerifier1Trace(pconfig) + if not args.bmc: + if args.onetrace: + pconfig, tmgr, module = start(PYCTask.VERIF1T, args) + verifier = JGVerifier1Trace(pconfig) + logger.debug("Running single trace verification.") + else: + pconfig, tmgr, module = start(PYCTask.VERIF2T, args) + verifier = JGVerifier2Trace(pconfig) + logger.debug("Running two trace verification.") else: - pconfig, tmgr, module = start(PYCTask.VERIF2T, args) - verifier = JGVerifier2Trace(pconfig) + pconfig, tmgr, module = start(PYCTask.VERIFBMC, args) + verifier = JGVerifier1TraceBMC(pconfig) + logger.debug("Running BMC verification.") verifier.verify(module) @@ -131,6 +137,12 @@ def main(args): argparser.add_argument( "-s", "--sdir", type=str, help="Directory to save results to.", default="" ) + argparser.add_argument( + "--port", + type=int, + help="Port number to connect to Jasper server", + default=8080 + ) verif.add_argument( "--onetrace", @@ -138,6 +150,12 @@ def main(args): action="store_true", default=False, ) + verif.add_argument( + "--bmc", + help="Perform verification with bounded model checking.", + action="store_true", + default=False, + ) for c in [verif, persynth, svagen, alignsynth, fullsynth]: c.add_argument( From 530c8c470a808a44ba95973bd3327a4c1e2bfb4a Mon Sep 17 00:00:00 2001 From: Adwait Godbole Date: Tue, 29 Oct 2024 20:26:23 -0700 Subject: [PATCH 2/8] (minor) bump CLI to use typer - fix: assumption enabling/disabling needs to know assms added by svagen - TODO: cleanup/make this more robust using a context --- pycaliper/jginterface/jgoracle.py | 20 ++-- pycaliper/pycmanager.py | 15 ++- pycaliper/svagen.py | 5 + pycaliper/verif/jgverifier.py | 6 +- pycmain.py | 169 ++++++++++++++---------------- requirements.txt | 2 + 6 files changed, 110 insertions(+), 107 deletions(-) diff --git a/pycaliper/jginterface/jgoracle.py b/pycaliper/jginterface/jgoracle.py index 096433c..95c2a56 100644 --- a/pycaliper/jginterface/jgoracle.py +++ b/pycaliper/jginterface/jgoracle.py @@ -105,7 +105,7 @@ def enable_assm(taskcon: str, assm: str): return res -def set_assm_induction_1t(taskcon: str, k: int): +def set_assm_induction_1t(taskcon: str, symbsim_assms: list[str]): """Enable only 1-trace assumptions (required for 1 trace properties) Args: @@ -115,10 +115,10 @@ def set_assm_induction_1t(taskcon: str, k: int): enable_assm(taskcon, "state_inv") disable_assm(taskcon, "input") disable_assm(taskcon, "state") - for i in range(k): - disable_assm(taskcon, f"step_{i}") + for assm in symbsim_assms: + disable_assm(taskcon, assm) -def set_assm_induction_2t(taskcon: str, k: int): +def set_assm_induction_2t(taskcon: str, symbsim_assms: list[str]): """Enable all assumptions required for 2 trace properties Args: @@ -128,18 +128,18 @@ def set_assm_induction_2t(taskcon: str, k: int): enable_assm(taskcon, "state") enable_assm(taskcon, "input_inv") enable_assm(taskcon, "state_inv") - for i in range(k): - disable_assm(taskcon, f"step_{i}") + for assm in symbsim_assms: + disable_assm(taskcon, assm) -def set_assm_bmc(taskcon: str, k: int): +def set_assm_bmc(taskcon: str, symbsim_assms: list[str]): """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 i in range(k): - enable_assm(taskcon, f"step_{i}") - + for assm in symbsim_assms: + enable_assm(taskcon, assm) + def prove_out_induction_1t(taskcon) -> ProofResult: return prove(taskcon, "output_inv") diff --git a/pycaliper/pycmanager.py b/pycaliper/pycmanager.py index 48453aa..e86004b 100644 --- a/pycaliper/pycmanager.py +++ b/pycaliper/pycmanager.py @@ -15,6 +15,8 @@ from pycaliper.jginterface import jasperclient as jgc from pycaliper.jginterface.jgoracle import setjwd +from pydantic import BaseModel + from .per.per import Module logger = logging.getLogger(__name__) @@ -29,6 +31,15 @@ class PYCTask(Enum): PERSYNTH = 5 FULLSYNTH = 6 +class PYCArgs(BaseModel): + path : str + mock : bool = False + params : str = "" + sdir : str = "" + port : int = 8080 + onetrace : bool = False + bmc : bool = False + @dataclass class PYConfig: @@ -231,7 +242,7 @@ def mock_or_connect(pyconfig: PYConfig, port: int) -> bool: return True -def get_pyconfig(config, args) -> PYConfig: +def get_pyconfig(config, args: PYCArgs) -> PYConfig: jasperc = config.get("jasper") specc = config.get("spec") tracec = config.get("trace", {}) @@ -259,7 +270,7 @@ def get_pyconfig(config, args) -> PYConfig: ) -def start(task: PYCTask, args) -> tuple[PYConfig, PYCManager, Module]: +def start(task: PYCTask, args: PYCArgs) -> tuple[PYConfig, PYCManager, Module]: with open(args.path, "r") as f: config = json.load(f) diff --git a/pycaliper/svagen.py b/pycaliper/svagen.py index a5d516d..2186725 100644 --- a/pycaliper/svagen.py +++ b/pycaliper/svagen.py @@ -81,6 +81,9 @@ def __init__(self, topmod: Module) -> None: self.holes: dict[str, PERHole] = {} + self.symbsim_assms = [] + self.symbsim_asrts = [] + def _generate_decls_for_per(self, per: PER): declbase = per.logic.get_hier_path_nonindex() declfull = per.logic.get_hier_path("_") @@ -290,6 +293,8 @@ def generate_step_decls(self, k: int, a: str = "a") -> list[str]: f"{TOP_STEP_ASSERT(i)} : assert property\n" + f"\t({step(i)} |-> {assert_spec});" ) + self.symbsim_asrts.append(step(i)) + self.symbsim_assms.append(step(i)) return properties diff --git a/pycaliper/verif/jgverifier.py b/pycaliper/verif/jgverifier.py index c98425c..790bfce 100644 --- a/pycaliper/verif/jgverifier.py +++ b/pycaliper/verif/jgverifier.py @@ -46,7 +46,7 @@ def verify(self, module) -> bool: for cand in self.candidates: disable_assm(self.psc.context, cand) # Enable the assumptions for 1 trace verification - set_assm_induction_1t(self.psc.context, self.psc.k) + set_assm_induction_1t(self.psc.context, self.svagen.symbsim_assms) res = is_pass(prove_out_induction_1t(self.psc.context)) res_str = "SAFE" if res else "UNSAFE" @@ -79,7 +79,7 @@ def verify(self, module): for cand in self.candidates: disable_assm(self.psc.context, cand) # Enable the assumptions for 2 trace verification - set_assm_induction_2t(self.psc.context, self.psc.k) + set_assm_induction_2t(self.psc.context, self.svagen.symbsim_assms) res = is_pass(prove_out_induction_2t(self.psc.context)) res_str = "SAFE" if res else "UNSAFE" @@ -112,7 +112,7 @@ def verify(self, module): for cand in self.candidates: disable_assm(self.psc.context, cand) # Enable the assumptions for 1 trace verification - set_assm_bmc(self.psc.context, self.psc.k) + set_assm_bmc(self.psc.context, self.svagen.symbsim_assms) results = [is_pass(r) for r in prove_out_bmc(self.psc.context, self.psc.k)] results_str = '\n\t'.join( diff --git a/pycmain.py b/pycmain.py index 1a3c634..fb1fc42 100644 --- a/pycmain.py +++ b/pycmain.py @@ -1,14 +1,15 @@ import sys -import argparse -import json import logging from pycaliper.verif.jgverifier import JGVerifier1Trace, JGVerifier2Trace, JGVerifier1TraceBMC from pycaliper.synth.persynthesis import PERSynthesizer from pycaliper.svagen import SVAGen from pycaliper.synth.alignsynthesis import AlignSynthesizer -from pycaliper.pycmanager import PYCManager, PYConfig, start, PYCTask +from pycaliper.pycmanager import start, PYCTask, PYCArgs +import typer +from typer import Argument, Option +from typing_extensions import Annotated h1 = logging.StreamHandler(sys.stdout) h1.setLevel(logging.INFO) @@ -23,10 +24,28 @@ logger = logging.getLogger(__name__) - -def verif_main(args): - if not args.bmc: - if args.onetrace: +DESCRIPTION = "Invariant verification and synthesis using Jasper." +app = typer.Typer(help=DESCRIPTION) + + +@app.command("verif") +def verif_main( + path: Annotated[str, Argument(help="Path to the JSON config file")] = "", + # Allow using -m or --mock + mock: Annotated[bool, Option("--mock", "-m", help="Run in offline (mock) mode?")] = False, + # Allow using --params + params: Annotated[str, Option(help="Parameters for the spec module: (=)+")] = "", + # Allow using -s or --sdir + sdir: Annotated[str, Option(help="Directory to save results to.")] = "", + # Allow using --port + port: Annotated[int, Option(help="Port number to connect to Jasper server")] = 8080, + # Allow using --onetrace + onetrace: Annotated[bool, Option(help="Verify only one-trace properties.")] = False, + # Allow using --bmc + bmc: Annotated[bool, Option(help="Perform verification with bounded model checking.")] = False): + args = PYCArgs(path=path, mock=mock, params=params, sdir=sdir, port=port, onetrace=onetrace, bmc=bmc) + if not bmc: + if onetrace: pconfig, tmgr, module = start(PYCTask.VERIF1T, args) verifier = JGVerifier1Trace(pconfig) logger.debug("Running single trace verification.") @@ -41,9 +60,19 @@ def verif_main(args): verifier.verify(module) - -def persynth_main(args): - +@app.command("persynth") +def persynth_main( + path: Annotated[str, Argument(help="Path to the JSON config file")] = "", + # Allow using -m or --mock + mock: Annotated[bool, Option("--mock", "-m", help="Run in offline (mock) mode?")] = False, + # Allow using --params + params: Annotated[str, Option(help="Parameters for the spec module: (=)+")] = "", + # Allow using -s or --sdir + sdir: Annotated[str, Option(help="Directory to save results to.")] = "", + # Allow using --port + port: Annotated[int, Option(help="Port number to connect to Jasper server")] = 8080): + + args = PYCArgs(path=path, mock=mock, params=params, sdir=sdir, port=port) pconfig, tmgr, module = start(PYCTask.PERSYNTH, args) synthesizer = PERSynthesizer(pconfig) @@ -53,14 +82,37 @@ def persynth_main(args): tmgr.save() -def svagen_main(args): +@app.command("svagen") +def svagen_main( + path: Annotated[str, Argument(help="Path to the JSON config file")] = "", + # Allow using -m or --mock + mock: Annotated[bool, Option("--mock", "-m", help="Run in offline (mock) mode?")] = False, + # Allow using --params + params: Annotated[str, Option(help="Parameters for the spec module: (=)+")] = "", + # Allow using -s or --sdir + sdir: Annotated[str, Option(help="Directory to save results to.")] = "", + # Allow using --port + port: Annotated[int, Option(help="Port number to connect to Jasper server")] = 8080): + args = PYCArgs(path=path, mock=mock, params=params, sdir=sdir, port=port) pconfig, tmgr, module = start(PYCTask.SVAGEN, args) svagen = SVAGen(module) svagen.create_pyc_specfile(k=pconfig.k, filename=pconfig.pycfile) -def alignsynth_main(args): +@app.command("alignsynth") +def alignsynth_main( + path: Annotated[str, Argument(help="Path to the JSON config file")] = "", + # Allow using -m or --mock + mock: Annotated[bool, Option("--mock", "-m", help="Run in offline (mock) mode?")] = False, + # Allow using --params + params: Annotated[str, Option(help="Parameters for the spec module: (=)+")] = "", + # Allow using -s or --sdir + sdir: Annotated[str, Option(help="Directory to save results to.")] = "", + # Allow using --port + port: Annotated[int, Option(help="Port number to connect to Jasper server")] = 8080): + args = PYCArgs(path=path, mock=mock, params=params, sdir=sdir, port=port) + pconfig, tmgr, module = start(PYCTask.CTRLSYNTH, args) synthesizer = AlignSynthesizer(tmgr, pconfig) @@ -70,7 +122,18 @@ def alignsynth_main(args): tmgr.save() -def fullsynth_main(args): +@app.command("fullsynth") +def fullsynth_main( + path: Annotated[str, Argument(help="Path to the JSON config file")] = "", + # Allow using -m or --mock + mock: Annotated[bool, Option("--mock", "-m", help="Run in offline (mock) mode?")] = False, + # Allow using --params + params: Annotated[str, Option(help="Parameters for the spec module: (=)+")] = "", + # Allow using -s or --sdir + sdir: Annotated[str, Option(help="Directory to save results to.")] = "", + # Allow using --port + port: Annotated[int, Option(help="Port number to connect to Jasper server")] = 8080): + args = PYCArgs(path=path, mock=mock, params=params, sdir=sdir, port=port) pconfig, tmgr, module = start(PYCTask.FULLSYNTH, args) # PER Synthesizer @@ -95,85 +158,7 @@ def fullsynth_main(args): # PER Synthesize module finalmod = psynth.synthesize(asmod) tmgr.save_spec(finalmod) - tmgr.save() - -def main(args): - - DESCRIPTION = "Invariant verification and synthesis using Jasper." - - argparser = argparse.ArgumentParser(description=DESCRIPTION) - - cmd = argparser.add_subparsers(dest="cmd") - - verif = cmd.add_parser("verif", help="Verify invariants.") - verif.set_defaults(func=verif_main) - persynth = cmd.add_parser("persynth", help="Synthesize invariants.") - persynth.set_defaults(func=persynth_main) - svagen = cmd.add_parser("svagen", help="Generate SVA spec file.") - svagen.set_defaults(func=svagen_main) - alignsynth = cmd.add_parser("alignsynth", help="Synthesize counter alignment.") - alignsynth.set_defaults(func=alignsynth_main) - fullsynth = cmd.add_parser( - "fullsynth", help="Synthesize 1t invariants followed by (cond)equality ones." - ) - fullsynth.set_defaults(func=fullsynth_main) - - argparser.add_argument("path", type=str, help="Path to the JSON config file") - argparser.add_argument( - "-m", - "--mock", - help="Run in offline (mock) mode?", - action="store_true", - default=False, - ) - argparser.add_argument( - "--params", - nargs="+", - help="Parameters for the spec module: (=)+", - default="", - ) - argparser.add_argument( - "-s", "--sdir", type=str, help="Directory to save results to.", default="" - ) - argparser.add_argument( - "--port", - type=int, - help="Port number to connect to Jasper server", - default=8080 - ) - - verif.add_argument( - "--onetrace", - help="Verify only one-trace properties.", - action="store_true", - default=False, - ) - verif.add_argument( - "--bmc", - help="Perform verification with bounded model checking.", - action="store_true", - default=False, - ) - - for c in [verif, persynth, svagen, alignsynth, fullsynth]: - c.add_argument( - "--params", - nargs="+", - help="Parameters for the spec module: (=)+", - default="", - ) - - args = argparser.parse_args(args) - - # Run main command - if args.cmd in ["verif", "persynth", "svagen", "alignsynth", "fullsynth"]: - args.func(args) - else: - argparser.print_help() - sys.exit(1) - - if __name__ == "__main__": - main(sys.argv[1:]) + app() diff --git a/requirements.txt b/requirements.txt index 495b713..bc8597b 100644 --- a/requirements.txt +++ b/requirements.txt @@ -19,3 +19,5 @@ referencing==0.35.1 rpds-py==0.20.0 vcdvcd==2.3.5 virtualenv==20.26.3 +pydantic==1.10.0 +typer==0.12.5 From 04c3fb7615aef258422012e0f010189fa381b8ae Mon Sep 17 00:00:00 2001 From: Adwait Godbole Date: Fri, 1 Nov 2024 12:37:20 -0700 Subject: [PATCH 3/8] minor: remove pyc SVA intermediate files --- .gitignore | 3 + designs/regblock/regblock.pyc.sv | 145 --------------------------- designs/regblock/regblock_old.pyc.sv | 52 ---------- 3 files changed, 3 insertions(+), 197 deletions(-) delete mode 100644 designs/regblock/regblock.pyc.sv delete mode 100644 designs/regblock/regblock_old.pyc.sv diff --git a/.gitignore b/.gitignore index 8b5fa4c..d1c7d04 100644 --- a/.gitignore +++ b/.gitignore @@ -10,5 +10,8 @@ __pycache__ dump +# SVA intermediate files +*.pyc.sv + # Jasper directory jgproject/ diff --git a/designs/regblock/regblock.pyc.sv b/designs/regblock/regblock.pyc.sv deleted file mode 100644 index abe8c09..0000000 --- a/designs/regblock/regblock.pyc.sv +++ /dev/null @@ -1,145 +0,0 @@ - - logic counter; - always @(posedge clk) begin - if (fvreset) begin - counter <= 0; - end else begin - if (counter < 1'd1) begin - counter <= (counter + 1'b1); - end - end - end - logic step = (counter == 1'd1); - -logic eq_reg1_rst ; -logic eq_reg1_en ; -logic condeq_reg1_d ; -logic eq_reg1_q ; -logic eq_reg2_rst ; -logic eq_reg2_en ; -logic condeq_reg2_d ; -logic eq_reg2_q ; -logic eq_rst ; -logic eq_en ; -logic condeq_d ; -logic condeq_wr_index ; -logic eq_rd_index ; -logic eq_q ; -assign eq_reg1_rst = (a.reg1.rst == b.reg1.rst); -assign eq_reg1_en = (a.reg1.en == b.reg1.en); -assign condeq_reg1_d = (!(a.reg1.en && b.reg1.en) | (a.reg1.d == b.reg1.d)); -assign eq_reg1_q = (a.reg1.q == b.reg1.q); -assign eq_reg2_rst = (a.reg2.rst == b.reg2.rst); -assign eq_reg2_en = (a.reg2.en == b.reg2.en); -assign condeq_reg2_d = (!(a.reg2.en && b.reg2.en) | (a.reg2.d == b.reg2.d)); -assign eq_reg2_q = (a.reg2.q == b.reg2.q); -assign eq_rst = (a.rst == b.rst); -assign eq_en = (a.en == b.en); -assign condeq_d = (!(a.en && b.en) | (a.d == b.d)); -assign condeq_wr_index = (!(a.en && b.en) | (a.wr_index == b.wr_index)); -assign eq_rd_index = (a.rd_index == b.rd_index); -assign eq_q = (a.q == b.q); - -///////////////////////////////////// -// Module reg1 - -wire reg1_input = ( - eq_reg1_rst && - eq_reg1_en && - condeq_reg1_d && - 1'b1); -wire reg1_state = ( - eq_reg1_q && - 1'b1); -wire reg1_output = ( - eq_reg1_q && - 1'b1); -wire reg1_input_inv = ( - 1'b1); -wire reg1_state_inv = ( - 1'b1); -wire reg1_output_inv = ( - 1'b1); -wire reg1_input_inv = ( - 1'b1); -wire reg1_state_inv = ( - 1'b1); -wire reg1_output_inv = ( - 1'b1); - -///////////////////////////////////// -// Module reg2 - -wire reg2_input = ( - eq_reg2_rst && - eq_reg2_en && - condeq_reg2_d && - 1'b1); -wire reg2_state = ( - eq_reg2_q && - 1'b1); -wire reg2_output = ( - eq_reg2_q && - 1'b1); -wire reg2_input_inv = ( - 1'b1); -wire reg2_state_inv = ( - 1'b1); -wire reg2_output_inv = ( - 1'b1); -wire reg2_input_inv = ( - 1'b1); -wire reg2_state_inv = ( - 1'b1); -wire reg2_output_inv = ( - 1'b1); - -///////////////////////////////////// -// Module - -wire _input = ( - eq_rst && - eq_en && - condeq_d && - condeq_wr_index && - eq_rd_index && - 1'b1); -wire _state = ( - eq_reg1_q && - eq_reg2_q && - 1'b1); -wire _output = ( - eq_q && - 1'b1); -wire _input_inv = ( - 1'b1); -wire _state_inv = ( - 1'b1); -wire _output_inv = ( - 1'b1); -wire _input_inv = ( - 1'b1); -wire _state_inv = ( - 1'b1); -wire _output_inv = ( - 1'b1); - -///////////////////////////////////// -// Assumptions and Assertions for top module -A_input_inv : assume property - (_input_inv); - -A_state_inv : assume property - (!(step) |-> (_state_inv)); - -P_output_inv : assert property - (step |-> (_state_inv && _output_inv)); - -A_input : assume property - (_input && _input_inv); - -A_state : assume property - (!(step) |-> (_state && _state_inv)); - -P_output : assert property - (step |-> (_state && _state_inv && _output && _output_inv)); diff --git a/designs/regblock/regblock_old.pyc.sv b/designs/regblock/regblock_old.pyc.sv deleted file mode 100644 index 348b5fe..0000000 --- a/designs/regblock/regblock_old.pyc.sv +++ /dev/null @@ -1,52 +0,0 @@ - logic step; - always @(posedge clk ) begin - if (fvreset) begin - step <= 0; - end else begin - step <= 1; - end - end - - - -////////////////////////////////////////////////////////////////////// -// regblock module - -wire _input = - a.rst == b.rst && - a.rd_index == b.rd_index && - a.wr_index == b.wr_index && - a.en == b.en && - a.d == b.d && - 1'b1; - -wire eq_q = (a.q == b.q); -wire eq_reg1_q = (a.reg1.q == b.reg1.q); -wire eq_reg2_q = (a.reg2.q == b.reg2.q); - -wire _output = - eq_q && eq_reg1_q && eq_reg2_q; - -A_input : assume property - (_input); - -A_eq_q : assume property - (!step |-> eq_q); - -A_eq_reg1_q : assume property - (!step |-> eq_reg1_q); - -A_eq_reg2_q : assume property - (!step |-> eq_reg2_q); - -P_eq_q : assert property - (step |-> eq_q); - -P_eq_reg1_q : assert property - (step |-> eq_reg1_q); - -P_eq_reg2_q : assert property - (step |-> eq_reg2_q); - -P_output : assert property - (step |-> _output); From 593861066f2c77c9554fa7b55ee34b8a378df900 Mon Sep 17 00:00:00 2001 From: Adwait Godbole Date: Fri, 1 Nov 2024 12:53:16 -0700 Subject: [PATCH 4/8] example: add adder module and specs --- designs/adder/adder.sv | 25 +++++++++++ designs/adder/adder.tcl | 85 ++++++++++++++++++++++++++++++++++++++ designs/adder/config.json | 12 ++++++ designs/adder/design.lst | 1 + designs/adder/one_trace.sv | 20 +++++++++ pycaliper/svagen.py | 15 ++++--- specs/adder.py | 40 ++++++++++++++++++ 7 files changed, 192 insertions(+), 6 deletions(-) create mode 100644 designs/adder/adder.sv create mode 100644 designs/adder/adder.tcl create mode 100644 designs/adder/config.json create mode 100644 designs/adder/design.lst create mode 100644 designs/adder/one_trace.sv create mode 100644 specs/adder.py diff --git a/designs/adder/adder.sv b/designs/adder/adder.sv new file mode 100644 index 0000000..3f7c4bb --- /dev/null +++ b/designs/adder/adder.sv @@ -0,0 +1,25 @@ + + +module adder #( + parameter int unsigned WIDTH = 8 +) ( + input logic clk_i, + input logic rst_ni, + input logic [WIDTH-1:0] a_i, + input logic [WIDTH-1:0] b_i, + output logic [WIDTH-1:0] sum_o +); + + logic [WIDTH:0] sum; + + always_ff @(posedge clk_i or negedge rst_ni) begin + if (!rst_ni) begin + sum <= '0; + end else begin + sum <= a_i + b_i; + end + end + + assign sum_o = sum[WIDTH-1:0]; + +endmodule \ No newline at end of file diff --git a/designs/adder/adder.tcl b/designs/adder/adder.tcl new file mode 100644 index 0000000..ac95aa3 --- /dev/null +++ b/designs/adder/adder.tcl @@ -0,0 +1,85 @@ +set banner "========== New session ==========" +puts $banner + +clear -all + +# Disable some info messages and warning messages +# set_message -disable VERI-9033 ; # array automatically black-boxed +# set_message -disable WNL008 ; # module is undefined. All instances will be black-boxed +# set_message -disable VERI-1002 ; # Can't disable this error message (net does not have a driver) +# set_message -disable VERI-1407 ; # attribute target identifier not found in this scope +set_message -disable VERI-1018 ; # info +set_message -disable VERI-1328 ; # info +set_message -disable VERI-2571 ; # info +# set_message -disable VERI-2571 ; # info: disabling old hierarchical reference handler +set_message -disable INL011 ; # info: processing file +# set_message -disable VERI-1482 ; # analyzing verilog file +set_message -disable VERI-1141 ; # system task is not supported +set_message -disable VERI-1060 ; # 'initial' construct is ignored +set_message -disable VERI-1142 ; # system task is ignored for synthesis +# set_message -disable ISW003 ; # top module name +# set_message -disable HIER-8002 ; # disabling old hierarchical reference handler +set_message -disable WNL046 ; # renaming embedded assertions due to name conflicts +set_message -disable VERI-1995 ; # unique/priority if/case is not full + # (we check these conditions with the elaborate + # option -extract_case_assertions) + +set JASPER_FILES { + one_trace.sv +} + +set env(DESIGN_HOME) [pwd]/.. +set err_status [catch {analyze -sv12 +define+JASPER +define+SYNTHESIS +libext+.v+.sv+.vh+.svh+ -f design.lst {*}$JASPER_FILES} err_msg] +if $err_status {error $err_msg} + +elaborate \ + -top einter \ + -extract_case_assertions \ + -no_preconditions \ + +proc write_reset_seq {file} { + puts $file "fvreset 1'b1" + puts $file 1 + puts $file "fvreset 1'b0" + puts $file {$} + close $file +} + +proc reset_formal {} { + write_reset_seq [open "reset.rseq" w] + # reset -expression fvreset + reset -sequence "reset.rseq" +} + + +clock clk + +# Constrain primary inputs to only change on @(posedge eph1) +clock -rate -default clk + +reset_formal + +# Set default Jasper proof engines (overrides use_nb engine settings) +#set_engine_mode {Ht Hp B K I N D AG AM Tri} +set_engine_mode {Ht} + +set_max_trace_length 3 + +# Adds $prefix to each string in $list +proc map_prefix {prefix list} { + set out {} + foreach s $list { + lappend out "${prefix}${s}" + } + return $out +} + +# The input signals of a module instance +proc instance_inputs {inst} { + map_prefix "${inst}." [get_design_info -instance $inst -list input -silent] +} + +# The output signals of a module instance +proc instance_outputs {inst} { + map_prefix "${inst}." [get_design_info -instance $inst -list output -silent] +} diff --git a/designs/adder/config.json b/designs/adder/config.json new file mode 100644 index 0000000..28fa081 --- /dev/null +++ b/designs/adder/config.json @@ -0,0 +1,12 @@ +{ + "jasper" : { + "jdir" : "designs/adder", + "script" : "adder.tcl", + "pycfile" : "adder.pyc.sv", + "context" : "::einter" + }, + "spec" : { + "pycspec" : "adder", + "k" : 2 + } +} diff --git a/designs/adder/design.lst b/designs/adder/design.lst new file mode 100644 index 0000000..8986a03 --- /dev/null +++ b/designs/adder/design.lst @@ -0,0 +1 @@ +${DESIGN_HOME}/adder/adder.sv diff --git a/designs/adder/one_trace.sv b/designs/adder/one_trace.sv new file mode 100644 index 0000000..06072fd --- /dev/null +++ b/designs/adder/one_trace.sv @@ -0,0 +1,20 @@ +// Parent module with a miter with different inputs +module einter ( + input wire clk +); + + + adder #( + .WIDTH(8) + ) adder_0 ( + .clk_i(clk) + ); + + default clocking cb @(posedge clk); + endclocking // cb + + logic fvreset; + + `include "adder.pyc.sv" + +endmodule diff --git a/pycaliper/svagen.py b/pycaliper/svagen.py index 2186725..d1b26dc 100644 --- a/pycaliper/svagen.py +++ b/pycaliper/svagen.py @@ -13,9 +13,12 @@ COUNTER = "_pycinternal__counter" STEP = "_pycinternal__step" -def step(k: int): +def step_signal(k: int): return f"{STEP}_{k}" +def step_property(k: int): + return f"step_{k}" + def eq_sva(s: str): return f"eq_{s}" @@ -287,14 +290,14 @@ def generate_step_decls(self, k: int, a: str = "a") -> list[str]: properties.append( f"{TOP_STEP_ASSUME(i)} : assume property\n" - + f"\t({step(i)} |-> {assume_spec});" + + f"\t({step_signal(i)} |-> {assume_spec});" ) properties.append( f"{TOP_STEP_ASSERT(i)} : assert property\n" - + f"\t({step(i)} |-> {assert_spec});" + + f"\t({step_signal(i)} |-> {assert_spec});" ) - self.symbsim_asrts.append(step(i)) - self.symbsim_assms.append(step(i)) + self.symbsim_asrts.append(step_property(i)) + self.symbsim_assms.append(step_property(i)) return properties @@ -316,7 +319,7 @@ def counter_step(self, k: int): \tlogic {STEP} = ({COUNTER} == {counter_width}'d{k}); """ for i in range(k): - vlog += f"\tlogic {step(i)} = ({COUNTER} == {counter_width}'d{i});\n" + vlog += f"\tlogic {step_signal(i)} = ({COUNTER} == {counter_width}'d{i});\n" return vlog diff --git a/specs/adder.py b/specs/adder.py new file mode 100644 index 0000000..5e965cf --- /dev/null +++ b/specs/adder.py @@ -0,0 +1,40 @@ + + +from pycaliper.per import * +from pycaliper.per.per import unroll + + +from random import randint + +class adder(Module): + + def __init__(self, **kwargs): + super().__init__() + # default width is 8 + self.width = kwargs.get("width", 8) + + self.rst_ni = Logic(1) + + self.a_i = Logic(self.width) + self.b_i = Logic(self.width) + self.sum_o = Logic(self.width) + + self.probe_inputs = [randint(0, 2**self.width - 1) for _ in range(2)] + + + def get_reset_seq(self, i: int) -> None: + if i == 0: + self.pycassume(~self.rst_ni) + else: + self.pycassume(self.rst_ni) + + @unroll(3) + def simstep(self, i: int = 0) -> None: + if i == 1: + self.pycassume(self.a_i == Const(self.probe_inputs[0], self.width)) + self.pycassume(self.b_i == Const(self.probe_inputs[1], self.width)) + elif i == 2: + self.pycassert(self.sum_o == Const((self.probe_inputs[0] + self.probe_inputs[1]) % (2**self.width), self.width)) + + self.get_reset_seq(i) + \ No newline at end of file From 8ee5e0746fbe009f3e46d1ab836400f6ea9a246f Mon Sep 17 00:00:00 2001 From: Adwait Godbole Date: Fri, 1 Nov 2024 13:55:48 -0700 Subject: [PATCH 5/8] test: add test for symvolic simulation - fix: BMC depth and module instance name --- designs/adder/adder.tcl | 2 +- designs/adder/config.json | 2 +- designs/adder/one_trace.sv | 2 +- tests/test.py | 49 +++++++++++++++++++++++++++++++------- 4 files changed, 44 insertions(+), 11 deletions(-) diff --git a/designs/adder/adder.tcl b/designs/adder/adder.tcl index ac95aa3..548c30f 100644 --- a/designs/adder/adder.tcl +++ b/designs/adder/adder.tcl @@ -63,7 +63,7 @@ reset_formal #set_engine_mode {Ht Hp B K I N D AG AM Tri} set_engine_mode {Ht} -set_max_trace_length 3 +set_max_trace_length 4 # Adds $prefix to each string in $list proc map_prefix {prefix list} { diff --git a/designs/adder/config.json b/designs/adder/config.json index 28fa081..67fb962 100644 --- a/designs/adder/config.json +++ b/designs/adder/config.json @@ -7,6 +7,6 @@ }, "spec" : { "pycspec" : "adder", - "k" : 2 + "k" : 3 } } diff --git a/designs/adder/one_trace.sv b/designs/adder/one_trace.sv index 06072fd..c3126a3 100644 --- a/designs/adder/one_trace.sv +++ b/designs/adder/one_trace.sv @@ -6,7 +6,7 @@ module einter ( adder #( .WIDTH(8) - ) adder_0 ( + ) a ( .clk_i(clk) ); diff --git a/tests/test.py b/tests/test.py index 3be8287..ea80470 100644 --- a/tests/test.py +++ b/tests/test.py @@ -11,7 +11,7 @@ from tempfile import NamedTemporaryFile -from pycaliper.pycmanager import get_pyconfig +from pycaliper.pycmanager import get_pyconfig, PYCArgs, PYCTask, start from pycaliper.frontend.pyclex import lexer from pycaliper.frontend.pycparse import parser @@ -22,6 +22,7 @@ import pycaliper.jginterface.jasperclient as jgc from pycaliper.btorinterface.pycbtorsymex import PYCBTORSymex from pycaliper.verif.btorverifier import BTORVerifier2Trace +from pycaliper.verif.jgverifier import JGVerifier1TraceBMC from btor2ex import BoolectorSolver from btor2ex.btor2ex.utils import parsewrapper @@ -29,15 +30,30 @@ from specs.regblock import regblock from specs.array_nonzerobase import array_nonzerobase +# h1 = logging.StreamHandler(sys.stdout) +# h1.setLevel(logging.DEBUG) + +# # Info log to stdout + +# h1 = logging.FileHandler("debug.log", mode="w+") +# logging.basicConfig( +# level=logging.DEBUG, +# handlers=[h1], +# format="%(asctime)s::%(name)s::%(levelname)s::%(message)s", +# ) + +# logger = logging.getLogger(__name__) + h1 = logging.StreamHandler(sys.stdout) -h1.setLevel(logging.DEBUG) +h1.setLevel(logging.INFO) +h1.setFormatter(logging.Formatter("%(levelname)s::%(message)s")) + +h2 = logging.FileHandler("test_debug.log", mode="w") +h2.setLevel(logging.DEBUG) +h2.setFormatter(logging.Formatter("%(asctime)s::%(name)s::%(levelname)s::%(message)s")) -h1 = logging.FileHandler("debug.log", mode="w+") -logging.basicConfig( - level=logging.DEBUG, - handlers=[h1], - format="%(asctime)s::%(name)s::%(levelname)s::%(message)s", -) +# Add filename and line number to log messages +logging.basicConfig(level=logging.DEBUG, handlers=[h1, h2]) logger = logging.getLogger(__name__) @@ -124,6 +140,23 @@ def test_btorverifier1(self): engine = BTORVerifier2Trace(PYCBTORSymex(BoolectorSolver("test"), prgm)) self.assertTrue(engine.verify(regblock())) +class SymbolicSimulator(unittest.TestCase): + + def gen_test(self, path): + args = PYCArgs(path=path, mock=False, params="", sdir="", port=8080, onetrace=True, bmc=True) + return start(PYCTask.VERIFBMC, args) + + def test_adder(self): + (pconfig, tmgr, module) = self.gen_test("designs/adder/config.json") + + verifier = JGVerifier1TraceBMC(pconfig) + logger.debug("Running BMC verification.") + + verifier.verify(module) + + + + if __name__ == "__main__": unittest.main() From dcab4cd3ff8e520b35699c25be14fa2529304bcc Mon Sep 17 00:00:00 2001 From: Adwait Godbole Date: Fri, 1 Nov 2024 14:02:16 -0700 Subject: [PATCH 6/8] fix: remove commented code --- tests/test.py | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/tests/test.py b/tests/test.py index ea80470..19f5da3 100644 --- a/tests/test.py +++ b/tests/test.py @@ -30,20 +30,6 @@ from specs.regblock import regblock from specs.array_nonzerobase import array_nonzerobase -# h1 = logging.StreamHandler(sys.stdout) -# h1.setLevel(logging.DEBUG) - -# # Info log to stdout - -# h1 = logging.FileHandler("debug.log", mode="w+") -# logging.basicConfig( -# level=logging.DEBUG, -# handlers=[h1], -# format="%(asctime)s::%(name)s::%(levelname)s::%(message)s", -# ) - -# logger = logging.getLogger(__name__) - h1 = logging.StreamHandler(sys.stdout) h1.setLevel(logging.INFO) h1.setFormatter(logging.Formatter("%(levelname)s::%(message)s")) From d01d76f5babd98c60f68e7e85525c51b505571a4 Mon Sep 17 00:00:00 2001 From: Adwait Godbole Date: Fri, 1 Nov 2024 17:10:46 -0700 Subject: [PATCH 7/8] enh: cleanup SVAGen <-> Jasper interface with SVAContext that maintains "live" SV assumptions and properties --- pycaliper/jginterface/jgoracle.py | 68 +++++++++---------- pycaliper/propns.py | 25 +++++++ pycaliper/pycmanager.py | 4 +- pycaliper/svagen.py | 104 ++++++++++++++++-------------- pycaliper/synth/persynthesis.py | 4 +- pycaliper/verif/jgverifier.py | 15 +---- 6 files changed, 117 insertions(+), 103 deletions(-) create mode 100644 pycaliper/propns.py diff --git a/pycaliper/jginterface/jgoracle.py b/pycaliper/jginterface/jgoracle.py index 95c2a56..ab22605 100644 --- a/pycaliper/jginterface/jgoracle.py +++ b/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,7 +85,7 @@ 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) @@ -105,39 +93,47 @@ def enable_assm(taskcon: str, assm: str): 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) diff --git a/pycaliper/propns.py b/pycaliper/propns.py new file mode 100644 index 0000000..5a9dfd4 --- /dev/null +++ b/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}" diff --git a/pycaliper/pycmanager.py b/pycaliper/pycmanager.py index e86004b..a89c8bc 100644 --- a/pycaliper/pycmanager.py +++ b/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)? diff --git a/pycaliper/svagen.py b/pycaliper/svagen.py index d1b26dc..7976f25 100644 --- a/pycaliper/svagen.py +++ b/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,6 +66,15 @@ 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 @@ -84,8 +82,7 @@ def __init__(self, topmod: Module) -> None: 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" diff --git a/pycaliper/synth/persynthesis.py b/pycaliper/synth/persynthesis.py index 3950d18..1c1b7ac 100644 --- a/pycaliper/synth/persynthesis.py +++ b/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() diff --git a/pycaliper/verif/jgverifier.py b/pycaliper/verif/jgverifier.py index 790bfce..1f60e5a 100644 --- a/pycaliper/verif/jgverifier.py +++ b/pycaliper/verif/jgverifier.py @@ -42,11 +42,8 @@ def verify(self, module) -> bool: self.candidates = self.svagen.holes loadscript(self.psc.script) - # Disable all holes in the specification - for cand in self.candidates: - disable_assm(self.psc.context, cand) # Enable the assumptions for 1 trace verification - set_assm_induction_1t(self.psc.context, self.svagen.symbsim_assms) + set_assm_induction_1t(self.psc.context, self.svagen.property_context) res = is_pass(prove_out_induction_1t(self.psc.context)) res_str = "SAFE" if res else "UNSAFE" @@ -75,11 +72,8 @@ def verify(self, module): self.candidates = self.svagen.holes loadscript(self.psc.script) - # Disable all holes in the specification - for cand in self.candidates: - disable_assm(self.psc.context, cand) # Enable the assumptions for 2 trace verification - set_assm_induction_2t(self.psc.context, self.svagen.symbsim_assms) + set_assm_induction_2t(self.psc.context, self.svagen.property_context) res = is_pass(prove_out_induction_2t(self.psc.context)) res_str = "SAFE" if res else "UNSAFE" @@ -108,11 +102,8 @@ def verify(self, module): self.candidates = self.svagen.holes loadscript(self.psc.script) - # Disable all holes in the specification - for cand in self.candidates: - disable_assm(self.psc.context, cand) # Enable the assumptions for 1 trace verification - set_assm_bmc(self.psc.context, self.svagen.symbsim_assms) + set_assm_bmc(self.psc.context, self.svagen.property_context) results = [is_pass(r) for r in prove_out_bmc(self.psc.context, self.psc.k)] results_str = '\n\t'.join( From 1d522358350d83335c825d0304e16bedfc41352b Mon Sep 17 00:00:00 2001 From: Adwait Godbole Date: Mon, 4 Nov 2024 14:10:04 -0800 Subject: [PATCH 8/8] feat(auxmodules): Allow helper modules that enable easy refinement proofs: - `AuxModule`: an external Module that is hooked up at the top level: - allows addition of auxilliary (extra) signals - specifications can refer to these signals - example: `designs/counter` and `specs/counter.py` fix(onetrace): One trace verification needs to only dump properties with one instance TODO: clean-up the PyConfig and TaskMgr classes, they can most probably be combined, making interfaces simpler Signed-off-by: Adwait Godbole --- .gitignore | 1 + designs/counter/config.json | 12 +++++ designs/counter/counter.sv | 43 ++++++++++++++++ designs/counter/counter.tcl | 85 +++++++++++++++++++++++++++++++ designs/counter/design.lst | 1 + designs/counter/one_trace.sv | 17 +++++++ pycaliper/per/__init__.py | 2 + pycaliper/per/per.py | 95 +++++++++++++++++++++++++++++++---- pycaliper/pycmanager.py | 48 ++++++++++++------ pycaliper/svagen.py | 59 ++++++++++++++++------ pycaliper/verif/jgverifier.py | 15 ++++-- specs/counter.py | 39 ++++++++++++++ tests/test.py | 57 ++++++++++++--------- 13 files changed, 407 insertions(+), 67 deletions(-) create mode 100644 designs/counter/config.json create mode 100644 designs/counter/counter.sv create mode 100644 designs/counter/counter.tcl create mode 100644 designs/counter/design.lst create mode 100644 designs/counter/one_trace.sv create mode 100644 specs/counter.py diff --git a/.gitignore b/.gitignore index d1c7d04..7243aa5 100644 --- a/.gitignore +++ b/.gitignore @@ -12,6 +12,7 @@ dump # SVA intermediate files *.pyc.sv +reset.rseq # Jasper directory jgproject/ diff --git a/designs/counter/config.json b/designs/counter/config.json new file mode 100644 index 0000000..0128bd0 --- /dev/null +++ b/designs/counter/config.json @@ -0,0 +1,12 @@ +{ + "jasper" : { + "jdir" : "designs/counter", + "script" : "counter.tcl", + "pycfile" : "counter.pyc.sv", + "context" : "::einter" + }, + "spec" : { + "pycspec" : "counter", + "k" : 3 + } +} diff --git a/designs/counter/counter.sv b/designs/counter/counter.sv new file mode 100644 index 0000000..818535d --- /dev/null +++ b/designs/counter/counter.sv @@ -0,0 +1,43 @@ + + +module counter ( + input clk, + input rst, + output [7:0] counter +); + + // Counter that increments by 1 + logic [7:0] counter_internal; + + always_ff @(posedge clk or posedge rst) begin + if (rst) begin + counter_internal <= 8'h00; + end else begin + counter_internal <= counter_internal + 1; + end + end + + assign counter = counter_internal; + +endmodule + + +module parity ( + input clk, + input rst, + input [7:0] counter +); + + // OddEven parity + logic parity; + + // toggle parity bit + always_ff @(posedge clk or posedge rst) begin + if (rst) begin + parity <= 1'b0; + end else begin + parity <= ~parity; + end + end + +endmodule diff --git a/designs/counter/counter.tcl b/designs/counter/counter.tcl new file mode 100644 index 0000000..9efc64e --- /dev/null +++ b/designs/counter/counter.tcl @@ -0,0 +1,85 @@ +set banner "========== New session ==========" +puts $banner + +clear -all + +# Disable some info messages and warning messages +# set_message -disable VERI-9033 ; # array automatically black-boxed +# set_message -disable WNL008 ; # module is undefined. All instances will be black-boxed +# set_message -disable VERI-1002 ; # Can't disable this error message (net does not have a driver) +# set_message -disable VERI-1407 ; # attribute target identifier not found in this scope +set_message -disable VERI-1018 ; # info +set_message -disable VERI-1328 ; # info +set_message -disable VERI-2571 ; # info +# set_message -disable VERI-2571 ; # info: disabling old hierarchical reference handler +set_message -disable INL011 ; # info: processing file +# set_message -disable VERI-1482 ; # analyzing verilog file +set_message -disable VERI-1141 ; # system task is not supported +set_message -disable VERI-1060 ; # 'initial' construct is ignored +set_message -disable VERI-1142 ; # system task is ignored for synthesis +# set_message -disable ISW003 ; # top module name +# set_message -disable HIER-8002 ; # disabling old hierarchical reference handler +set_message -disable WNL046 ; # renaming embedded assertions due to name conflicts +set_message -disable VERI-1995 ; # unique/priority if/case is not full + # (we check these conditions with the elaborate + # option -extract_case_assertions) + +set JASPER_FILES { + one_trace.sv +} + +set env(DESIGN_HOME) [pwd] +set err_status [catch {analyze -sv12 +define+JASPER +define+SYNTHESIS +libext+.v+.sv+.vh+.svh+ -f design.lst {*}$JASPER_FILES} err_msg] +if $err_status {error $err_msg} + +elaborate \ + -top einter \ + -extract_case_assertions \ + -no_preconditions \ + +proc write_reset_seq {file} { + puts $file "fvreset 1'b1" + puts $file 1 + puts $file "fvreset 1'b0" + puts $file {$} + close $file +} + +proc reset_formal {} { + write_reset_seq [open "reset.rseq" w] + # reset -expression fvreset + reset -sequence "reset.rseq" +} + + +clock clk + +# Constrain primary inputs to only change on @(posedge eph1) +clock -rate -default clk + +reset_formal + +# Set default Jasper proof engines (overrides use_nb engine settings) +#set_engine_mode {Ht Hp B K I N D AG AM Tri} +set_engine_mode {Ht} + +set_max_trace_length 4 + +# Adds $prefix to each string in $list +proc map_prefix {prefix list} { + set out {} + foreach s $list { + lappend out "${prefix}${s}" + } + return $out +} + +# The input signals of a module instance +proc instance_inputs {inst} { + map_prefix "${inst}." [get_design_info -instance $inst -list input -silent] +} + +# The output signals of a module instance +proc instance_outputs {inst} { + map_prefix "${inst}." [get_design_info -instance $inst -list output -silent] +} diff --git a/designs/counter/design.lst b/designs/counter/design.lst new file mode 100644 index 0000000..0a197c0 --- /dev/null +++ b/designs/counter/design.lst @@ -0,0 +1 @@ +${DESIGN_HOME}/counter.sv diff --git a/designs/counter/one_trace.sv b/designs/counter/one_trace.sv new file mode 100644 index 0000000..36dba3c --- /dev/null +++ b/designs/counter/one_trace.sv @@ -0,0 +1,17 @@ +// Parent module with a miter with different inputs +module einter ( + input wire clk +); + + counter a ( + .clk(clk) + ); + + default clocking cb @(posedge clk); + endclocking // cb + + logic fvreset; + + `include "counter.pyc.sv" + +endmodule diff --git a/pycaliper/per/__init__.py b/pycaliper/per/__init__.py index c0e8ea7..be75daa 100644 --- a/pycaliper/per/__init__.py +++ b/pycaliper/per/__init__.py @@ -14,6 +14,8 @@ PERHole, CtrAlignHole, SVFunc, + AuxPort, + AuxModule, rose, fell, ) diff --git a/pycaliper/per/per.py b/pycaliper/per/per.py index a59042b..d8b36c8 100644 --- a/pycaliper/per/per.py +++ b/pycaliper/per/per.py @@ -142,8 +142,9 @@ def __hash__(self) -> int: class TypedElem: """An element in the design hierarchy (Logic, LogicArray, Struct, ...) with a type.""" - def __init__(self): + def __init__(self, root: str = None): self.name = "" + self.root = root pass def instantiate(self, path: Path): @@ -159,7 +160,7 @@ def _typ(self): class Logic(Expr, TypedElem): """Class for single bitvectors/signals""" - def __init__(self, width: int = 1, name: str = "") -> None: + def __init__(self, width: int = 1, name: str = "", root: str = None) -> None: """ Args: width (int, optional): width of logic signal. Defaults to 1. @@ -173,6 +174,8 @@ def __init__(self, width: int = 1, name: str = "") -> None: self.path: Path = Path([]) # If member of a logic array, this is the parent array self.parent = None + # Root + self.root = root def instantiate(self, path: Path, parent: "LogicArray" = None) -> "Logic": """Instantiate the logic signal with a path and parent array @@ -212,6 +215,8 @@ def get_sva(self, pref: str = "a") -> str: Returns: str: SVA representation of the signal. """ + if self.root is not None: + return f"{self.root}.{self.get_hier_path()}" return f"{pref}.{self.get_hier_path()}" def is_arr_elem(self) -> bool: @@ -261,6 +266,7 @@ def __init__( size: int, base: int = 0, name: str = "", + root: str = None, ): """An array of logic signals @@ -402,17 +408,20 @@ def __repr__(self): class Struct(TypedElem): """Struct as seen in SV""" - def __init__(self, name="", **kwargs) -> None: + def __init__(self, name="", root: str = None, **kwargs) -> None: self.name = name self.params = kwargs self.path = Path([]) self._signals: dict[str, TypedElem] = {} self._pycinternal__state: list[PER] = [] + self.root = root def _typ(self): return self.__class__.__name__ def get_sva(self, pref: str = "a") -> str: + if self.root is not None: + return f"{self.root}.{self.name}" return f"{pref}.{self.name}" def __str__(self) -> str: @@ -661,13 +670,15 @@ def _lambda(per: PER): return _lambda + class SimulationStep: - def __init__(self) -> None: self._pycinternal__assume: list[Expr] = [] self._pycinternal__assert: list[Expr] = [] + def _assume(self, expr: Expr): self._pycinternal__assume.append(expr) + def _assert(self, expr: Expr): self._pycinternal__assert.append(expr) @@ -678,10 +689,15 @@ def wrapper(self: Module, *args): for i in range(b): self._pycinternal__simstep = SimulationStep() func(self, i) - self._pycinternal__simsteps.append(copy.deepcopy(self._pycinternal__simstep)) + self._pycinternal__simsteps.append( + copy.deepcopy(self._pycinternal__simstep) + ) + return wrapper + return unroll_decorator + class Module: """Module class for specifications related to a SV HW module""" @@ -714,12 +730,14 @@ def __init__(self, name="", **kwargs) -> None: self._pycinternal__output_invs: list[Inv] = [] # Non-invariant properties self._pycinternal__simsteps: list[SimulationStep] = [] - self._pycinternal__simstep : SimulationStep = SimulationStep() + self._pycinternal__simstep: SimulationStep = SimulationStep() # PER holes self._perholes: list[PERHole] = [] # CtrAlign holes self._caholes: list[CtrAlignHole] = [] + self._auxmodules: dict[str, AuxModule] = {} + # Invariant functions to be overloaded by descendant specification classes def input(self) -> None: pass @@ -856,8 +874,10 @@ def pycassert(self, expr: Expr) -> None: if self._context == Context.UNROLL: self._pycinternal__simstep._assert(expr) else: - logger.warning("pycassert can only be used in the unroll context, skipping.") - + logger.warning( + "pycassert can only be used in the unroll context, skipping." + ) + def pycassume(self, expr: Expr) -> None: """Add an assumption to the current context. @@ -867,8 +887,9 @@ def pycassume(self, expr: Expr) -> None: if self._context == Context.UNROLL: self._pycinternal__simstep._assume(expr) else: - logger.warning("pycassume can only be used in the unroll context, skipping.") - + logger.warning( + "pycassume can only be used in the unroll context, skipping." + ) def instantiate(self, path: Path = Path([])) -> "Module": """Instantiate the current Module. @@ -888,6 +909,7 @@ def instantiate(self, path: Path = Path([])) -> "Module": groupattrs = {} funcattrs = {} submoduleattrs = {} + auxmoduleattrs = {} for attr in dir(self): obj = getattr(self, attr) if ( @@ -907,6 +929,11 @@ def instantiate(self, path: Path = Path([])) -> "Module": if obj.name == "": obj.name = attr funcattrs[obj.name] = obj + elif isinstance(obj, AuxModule): + # Current module must be top level + if obj.name == "": + obj.name = attr + auxmoduleattrs[obj.name] = obj.instantiate(path.add_level(obj.name)) elif isinstance(obj, Module): if obj.name == "": obj.name = attr @@ -915,6 +942,7 @@ def instantiate(self, path: Path = Path([])) -> "Module": self._groups = groupattrs self._functions = funcattrs self._submodules = submoduleattrs + self._auxmodules = auxmoduleattrs # Call the specification generator methods. self._context = Context.INPUT self.input() @@ -956,7 +984,6 @@ def sprint(self): s += f"\t{i.per} ({i.ctx})\n" return s - def get_repr(self, reprs): # Find all submodules and structs that need to be defined reprs[self.__class__.__name__] = repr(self) @@ -1055,6 +1082,52 @@ def pprint(self): print(self.sprint()) +class AuxPort(Logic): + def __init__(self, width: int = 1, name: str = "", root: str = None) -> None: + super().__init__(width, name, root) + + +class AuxModule(Module): + def __init__(self, portmapping: dict[str, TypedElem], name="", **kwargs) -> None: + super().__init__(name, **kwargs) + self._pycinternal__ports = {} + self.portmapping = portmapping + + def instantiate(self, root: Path = Path([])) -> None: + self.path = Path([]) + for attr in dir(self): + obj = getattr(self, attr) + if isinstance(obj, AuxPort): + self._pycinternal__ports[obj.name] = obj.instantiate( + self.path.add_level(obj.name) + ) + obj.root = root.get_hier_path() + elif isinstance(obj, TypedElem): + obj.root = root.get_hier_path() + obj.instantiate(self.path.add_level(obj.name)) + # Check that all ports are mapped + for k in self.portmapping: + if k not in self._pycinternal__ports: + logger.error(f"Port {k} not found in {self.__class__.__name__}") + sys.exit(1) + return self + + def get_instance_str(self, bindm: str): + portbindings = [] + for k, v in self.portmapping.items(): + portbindings.append(f".{k}({bindm}.{v})") + portbindings = ",\n\t".join(portbindings) + + aux_mod_decl = f""" +// Module {self.get_hier_path()} +{self.__class__.__name__} {self.name} ( + // Bindings + {portbindings} +); +""" + return aux_mod_decl + + # SVA-specific functions past = SVFunc("$past") stable = SVFunc("$stable") diff --git a/pycaliper/pycmanager.py b/pycaliper/pycmanager.py index a89c8bc..84d14e7 100644 --- a/pycaliper/pycmanager.py +++ b/pycaliper/pycmanager.py @@ -30,14 +30,15 @@ class PYCTask(Enum): PERSYNTH = 5 FULLSYNTH = 6 + class PYCArgs(BaseModel): - path : str - mock : bool = False - params : str = "" - sdir : str = "" - port : int = 8080 - onetrace : bool = False - bmc : bool = False + path: str + mock: bool = False + params: str = "" + sdir: str = "" + port: int = 8080 + onetrace: bool = False + bmc: bool = False class PYConfig(BaseModel): @@ -64,6 +65,8 @@ class PYConfig(BaseModel): pycspec: str = "" # bound to use for the k-inductive proof k: int = 1 + # Use only one trace for verification + onetrace: bool = False # Directory of pre-provided traces tdir: str = "" @@ -81,9 +84,14 @@ def __init__(self, pyconfig: PYConfig): self.pycspec: str = pyconfig.pycspec # Previous VCD traces directory + self.pyconfig = pyconfig self.sdir = pyconfig.sdir - self.wdir = tempfile.TemporaryDirectory(prefix="pyc_wdir_").name + # Create a temporary directory for the run, grab the name, and clean it up + wdir = tempfile.TemporaryDirectory(prefix="pyc_wdir_") + self.wdir = wdir.name + wdir.cleanup() + logger.info(f"Working directory: {self.wdir}") self.tracedir = f"{self.wdir}/traces" self.specdir = f"{self.wdir}/specs" @@ -141,6 +149,13 @@ def save(self): # Copy wdir to sdir os.system(f"cp -r {self.wdir}/. {self.sdir}/") + def close(self): + # Close the socket + self.save() + if not self.pyconfig.mock: + jgc.close_tcp() + logger.info("PyCaliper run completed, socket closed.") + CONFIG_SCHEMA = { "type": "object", @@ -192,7 +207,7 @@ def save(self): def create_module(specc, args): """Dynamically import the spec module and create an instance of it.""" - specmod : str = specc["pycspec"] + specmod: str = specc["pycspec"] params = specc.get("params", {}) parsed_conf = {} @@ -202,9 +217,9 @@ def create_module(specc, args): params.update(parsed_conf) - if '/' in specmod: + if "/" in specmod: # Split the module name into the module name and the parent package - module_path, module_name = specmod.rsplit('/', 1) + module_path, module_name = specmod.rsplit("/", 1) # Check if the path exists if not os.path.isdir(module_path): @@ -212,14 +227,18 @@ def create_module(specc, args): exit(1) # Add the module path to sys.path sys.path.append(module_path) - + try: # Import the module using importlib module = importlib.import_module(module_name) - logger.debug(f"Successfully imported module: {module_name} from {module_path}") + logger.debug( + f"Successfully imported module: {module_name} from {module_path}" + ) return getattr(module, module_name)(**params) except ImportError as e: - logger.error(f"Error importing module {module_name} from {module_path}: {e}") + logger.error( + f"Error importing module {module_name} from {module_path}: {e}" + ) return None finally: # Clean up: remove the path from sys.path to avoid potential side effects @@ -259,6 +278,7 @@ def get_pyconfig(config, args: PYCArgs) -> PYConfig: # Spec config pycspec=specc["pycspec"], k=specc["k"], + onetrace=args.onetrace, # Tracing configuration # Location where traces are provided tdir=tracec.get("tdir", ""), diff --git a/pycaliper/svagen.py b/pycaliper/svagen.py index 7976f25..fb38306 100644 --- a/pycaliper/svagen.py +++ b/pycaliper/svagen.py @@ -6,7 +6,7 @@ import logging from pydantic import BaseModel -from .per import Module, Eq, Path, Context, PER, Inv, PERHole +from .per import Module, Eq, Path, Context, PER, Inv, PERHole, AuxModule from .propns import * logger = logging.getLogger(__name__) @@ -15,9 +15,12 @@ # Internal signals COUNTER = "_pycinternal__counter" STEP_SIGNAL = "_pycinternal__step" + + def step_signal(k: int): return f"{STEP_SIGNAL}_{k}" + # def step_property(k: int): # return f"step_{k}" @@ -25,9 +28,11 @@ def step_signal(k: int): def eq_sva(s: str): return f"eq_{s}" + def condeq_sva(s: str): return f"condeq_{s}" + def per_sva(mod: Module, ctx: Context): if ctx == Context.INPUT: return f"{mod.get_hier_path('_')}_input" @@ -75,6 +80,7 @@ class SVAContext(BaseModel): assms_bmc: list[str] = [] asrts_bmc: list[str] = [] + class SVAGen: def __init__(self, topmod: Module) -> None: self.topmod = topmod @@ -226,7 +232,8 @@ 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"{get_as_assm(TOP_INPUT_1T_PROP)} : 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( @@ -241,7 +248,8 @@ def generate_decls(self, a: str = "a", b: str = "b"): self.property_context.asrts_1trace.append(TOP_INPUT_1T_PROP) properties.append( - f"{get_as_assm(TOP_INPUT_2T_PROP)} : 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( @@ -286,12 +294,18 @@ def generate_step_decls(self, k: int, a: str = "a") -> list[str]: Returns: list[str]: List of properties for each step - """ + """ properties = [] for i in range(min(k, len(self.topmod._pycinternal__simsteps))): - assumes = [expr.get_sva(a) for expr in self.topmod._pycinternal__simsteps[i]._pycinternal__assume] + assumes = [ + expr.get_sva(a) + for expr in self.topmod._pycinternal__simsteps[i]._pycinternal__assume + ] assume_spec = "(\n\t" + " && \n\t".join(assumes + ["1'b1"]) + ")" - asserts = [expr.get_sva(a) for expr in self.topmod._pycinternal__simsteps[i]._pycinternal__assert] + asserts = [ + expr.get_sva(a) + for expr in self.topmod._pycinternal__simsteps[i]._pycinternal__assert + ] assert_spec = "(\n\t" + " && \n\t".join(asserts + ["1'b1"]) + ")" properties.append( @@ -304,7 +318,7 @@ def generate_step_decls(self, k: int, a: str = "a") -> list[str]: + f"\t({step_signal(i)} |-> {assert_spec});" ) self.property_context.asrts_bmc.append(TOP_STEP_PROP(i)) - + return properties def counter_step(self, k: int): @@ -328,8 +342,9 @@ def counter_step(self, k: int): vlog += f"\tlogic {step_signal(i)} = ({COUNTER} == {counter_width}'d{i});\n" return vlog - - def create_pyc_specfile(self, k: int, a="a", b="b", filename="temp.pyc.sv"): + def create_pyc_specfile( + self, k: int, a="a", b="b", filename="temp.pyc.sv", onetrace=False + ): vlog = self.counter_step(k) @@ -337,6 +352,11 @@ def create_pyc_specfile(self, k: int, a="a", b="b", filename="temp.pyc.sv"): properties, all_decls = self.generate_decls(a, b) properties.extend(self.generate_step_decls(k, a)) + aux_modules = [] + # Get auxiliary modules if any + for _, aux_mod in self.topmod._auxmodules.items(): + aux_modules.append(aux_mod.get_instance_str(a)) + with open(filename, "w") as f: f.write(vlog + "\n") @@ -345,6 +365,13 @@ def create_pyc_specfile(self, k: int, a="a", b="b", filename="temp.pyc.sv"): for decl in all_decls[1].values(): f.write(decl + "\n") + # Write auxiliary modules + f.write("\n") + f.write("/////////////////////////////////////\n") + f.write("// Auxiliary modules\n") + for aux_mod in aux_modules: + f.write(aux_mod + "\n") + for mod, spec in self.specs.items(): f.write("\n") f.write(f"/////////////////////////////////////\n") @@ -353,12 +380,14 @@ def create_pyc_specfile(self, k: int, a="a", b="b", filename="temp.pyc.sv"): f.write(spec.input_spec_decl + "\n") f.write(spec.state_spec_decl + "\n") f.write(spec.output_spec_decl + "\n") - f.write(spec.input_inv_spec_decl_comp + "\n") - f.write(spec.state_inv_spec_decl_comp + "\n") - f.write(spec.output_inv_spec_decl_comp + "\n") - f.write(spec.input_inv_spec_decl_single + "\n") - f.write(spec.state_inv_spec_decl_single + "\n") - f.write(spec.output_inv_spec_decl_single + "\n") + if not onetrace: + f.write(spec.input_inv_spec_decl_comp + "\n") + f.write(spec.state_inv_spec_decl_comp + "\n") + f.write(spec.output_inv_spec_decl_comp + "\n") + else: + f.write(spec.input_inv_spec_decl_single + "\n") + f.write(spec.state_inv_spec_decl_single + "\n") + f.write(spec.output_inv_spec_decl_single + "\n") f.write("\n") f.write("/////////////////////////////////////\n") diff --git a/pycaliper/verif/jgverifier.py b/pycaliper/verif/jgverifier.py index 1f60e5a..ea893c7 100644 --- a/pycaliper/verif/jgverifier.py +++ b/pycaliper/verif/jgverifier.py @@ -12,7 +12,7 @@ disable_assm, set_assm_induction_1t, set_assm_induction_2t, - set_assm_bmc + set_assm_bmc, ) from .invverifier import InvVerifier @@ -38,7 +38,9 @@ def verify(self, module) -> bool: """ self.svagen = svagen.SVAGen(module) - self.svagen.create_pyc_specfile(filename=self.psc.pycfile, k=self.psc.k) + self.svagen.create_pyc_specfile( + filename=self.psc.pycfile, k=self.psc.k, onetrace=True + ) self.candidates = self.svagen.holes loadscript(self.psc.script) @@ -80,6 +82,7 @@ def verify(self, module): logger.info(f"Two trace verification result: {res_str}") return res + class JGVerifier1TraceBMC(InvVerifier): """One trace property verifier with BMC""" @@ -106,7 +109,11 @@ def verify(self, module): set_assm_bmc(self.psc.context, self.svagen.property_context) results = [is_pass(r) for r in prove_out_bmc(self.psc.context, self.psc.k)] - results_str = '\n\t'.join( - [f"Step {i}: SAFE" if res else f"Step {i}: UNSAFE" for (i, res) in enumerate(results)]) + results_str = "\n\t".join( + [ + f"Step {i}: SAFE" if res else f"Step {i}: UNSAFE" + for (i, res) in enumerate(results) + ] + ) logger.info(f"One trace verification result:\n\t{results_str}") return results diff --git a/specs/counter.py b/specs/counter.py new file mode 100644 index 0000000..6c5c3f7 --- /dev/null +++ b/specs/counter.py @@ -0,0 +1,39 @@ +# auxmod.py + +from pycaliper.per import * +from pycaliper.per.per import TypedElem + + +class parity(AuxModule): + def __init__(self, portmapping: dict[str, TypedElem], name="", **kwargs) -> None: + super().__init__(portmapping, name, **kwargs) + self.clk = AuxPort(1, "clk") + self.rst = AuxPort(1, "rst") + self.counter = AuxPort(8, "counter") + self.parity = Logic(1, "parity") + + +class counter(Module): + def __init__(self, name="", **kwargs) -> None: + super().__init__(name, **kwargs) + self.clk = Logic(1, "clk") + self.rst = Logic(1, "rst") + self.counter = Logic(8, "counter") + + self.parity = parity( + { + "clk": self.clk, + "rst": self.rst, + "counter": self.counter, + }, + name="monitor", + ) + + def input(self) -> None: + pass + + def state(self) -> None: + self.inv(self.counter(0) == self.parity.parity) + + def output(self) -> None: + pass diff --git a/tests/test.py b/tests/test.py index 19f5da3..781f3cf 100644 --- a/tests/test.py +++ b/tests/test.py @@ -22,13 +22,14 @@ import pycaliper.jginterface.jasperclient as jgc from pycaliper.btorinterface.pycbtorsymex import PYCBTORSymex from pycaliper.verif.btorverifier import BTORVerifier2Trace -from pycaliper.verif.jgverifier import JGVerifier1TraceBMC +from pycaliper.verif.jgverifier import JGVerifier1TraceBMC, JGVerifier1Trace from btor2ex import BoolectorSolver from btor2ex.btor2ex.utils import parsewrapper from specs.regblock import regblock from specs.array_nonzerobase import array_nonzerobase +from specs.counter import counter h1 = logging.StreamHandler(sys.stdout) h1.setLevel(logging.INFO) @@ -45,35 +46,41 @@ class TestSVAGen(unittest.TestCase): - def gen_sva(self, mod): + def gen_sva(self, mod, svafile): svagen = SVAGen(mod) # Write to temporary file - with NamedTemporaryFile( - mode="w+", delete=False, suffix=".sv", dir="tests/out" - ) as f: + with open(f"tests/out/{svafile}", "w") as f: svagen.create_pyc_specfile(k=2, filename=f.name) print(f"Wrote SVA specification to temporary file {f.name}") def test_array_nonzerobase(self): - self.gen_sva(array_nonzerobase()) + self.gen_sva(array_nonzerobase(), "array_nonzerobase.pyc.sv") def test_regblock(self): - self.gen_sva(regblock()) + self.gen_sva(regblock(), "regblock.pyc.sv") + def test_auxmodule(self): + self.gen_sva(counter(), "counter.pyc.sv") -class TestVerifier(unittest.TestCase): - def test_regblock(self): - jgc.MODE = jgc.ClientMode.SIM - regb = regblock() - - with open("designs/regblock/config.json", "r") as f: - config = json.load(f) +class TestVerifier(unittest.TestCase): + def gen_test(self, path, mock=False): + args = PYCArgs( + path=path, mock=mock, params="", sdir="", port=8080, onetrace=True, bmc=True + ) + return start(PYCTask.VERIFBMC, args) - args = Namespace(mock=True, sdir="") - pyconfig = get_pyconfig(config, args) + def test_regblock(self): + (pyconfig, tmgr, regb) = self.gen_test("designs/regblock/config.json") invverif = JGVerifier2Trace(pyconfig) invverif.verify(regb) + tmgr.close() + + def test_counter(self): + (pyconfig, tmgr, counter) = self.gen_test("designs/counter/config.json") + invverif = JGVerifier1Trace(pyconfig) + invverif.verify(counter) + tmgr.close() class TestParser(unittest.TestCase): @@ -126,22 +133,26 @@ def test_btorverifier1(self): engine = BTORVerifier2Trace(PYCBTORSymex(BoolectorSolver("test"), prgm)) self.assertTrue(engine.verify(regblock())) + class SymbolicSimulator(unittest.TestCase): - def gen_test(self, path): - args = PYCArgs(path=path, mock=False, params="", sdir="", port=8080, onetrace=True, bmc=True) + args = PYCArgs( + path=path, + mock=False, + params="", + sdir="", + port=8080, + onetrace=True, + bmc=True, + ) return start(PYCTask.VERIFBMC, args) def test_adder(self): (pconfig, tmgr, module) = self.gen_test("designs/adder/config.json") - verifier = JGVerifier1TraceBMC(pconfig) logger.debug("Running BMC verification.") - verifier.verify(module) - - - + tmgr.close() if __name__ == "__main__":