From d01d76f5babd98c60f68e7e85525c51b505571a4 Mon Sep 17 00:00:00 2001 From: Adwait Godbole Date: Fri, 1 Nov 2024 17:10:46 -0700 Subject: [PATCH] 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(