diff --git a/.gitignore b/.gitignore index 8b5fa4c..7243aa5 100644 --- a/.gitignore +++ b/.gitignore @@ -10,5 +10,9 @@ __pycache__ dump +# SVA intermediate files +*.pyc.sv +reset.rseq + # Jasper directory jgproject/ 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..548c30f --- /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 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/adder/config.json b/designs/adder/config.json new file mode 100644 index 0000000..67fb962 --- /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" : 3 + } +} 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..c3126a3 --- /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) + ) a ( + .clk_i(clk) + ); + + default clocking cb @(posedge clk); + endclocking // cb + + logic fvreset; + + `include "adder.pyc.sv" + +endmodule 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/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); diff --git a/pycaliper/jginterface/jgoracle.py b/pycaliper/jginterface/jgoracle.py index 414786e..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,37 +93,62 @@ def enable_assm(taskcon: str, assm: str): return res -def enable_assm_1t(taskcon: 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") - - -def enable_assm_2t(taskcon: str): + 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, 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") - - -def prove_out_1t(taskcon): + # 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, svacon: SVAContext): + """Enable all assumptions required for 1 BMC trace properties""" + # 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) + + +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/__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 0d3d456..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: @@ -607,6 +616,7 @@ class Context(Enum): INPUT = 0 STATE = 1 OUTPUT = 2 + UNROLL = 3 class Hole: @@ -661,6 +671,33 @@ 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,11 +728,16 @@ 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 self._caholes: list[CtrAlignHole] = [] + self._auxmodules: dict[str, AuxModule] = {} + # Invariant functions to be overloaded by descendant specification classes def input(self) -> None: pass @@ -706,6 +748,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 +865,32 @@ 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. @@ -838,6 +909,7 @@ def instantiate(self, path: Path = Path([])) -> "Module": groupattrs = {} funcattrs = {} submoduleattrs = {} + auxmoduleattrs = {} for attr in dir(self): obj = getattr(self, attr) if ( @@ -857,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 @@ -865,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() @@ -872,6 +950,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 @@ -1001,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/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 c40a819..84d14e7 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 @@ -15,6 +14,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__) @@ -24,13 +25,23 @@ class PYCTask(Enum): SVAGEN = 0 VERIF1T = 1 VERIF2T = 2 - CTRLSYNTH = 3 - PERSYNTH = 4 - FULLSYNTH = 5 + VERIFBMC = 3 + CTRLSYNTH = 4 + 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: +class PYConfig(BaseModel): """PyCaliper configuration class""" # Is this a mock run (without Jasper access)? @@ -54,6 +65,8 @@ class PYConfig: 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 = "" @@ -71,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" @@ -131,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", @@ -181,7 +206,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,21 +217,49 @@ 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 -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", {}) @@ -224,6 +278,7 @@ def get_pyconfig(config, args) -> PYConfig: # Spec config pycspec=specc["pycspec"], k=specc["k"], + onetrace=args.onetrace, # Tracing configuration # Location where traces are provided tdir=tracec.get("tdir", ""), @@ -233,7 +288,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) @@ -252,8 +307,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..fb38306 100644 --- a/pycaliper/svagen.py +++ b/pycaliper/svagen.py @@ -4,13 +4,27 @@ import sys import logging -from dataclasses import dataclass +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__) +# 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}" + +# Internal wire names def eq_sva(s: str): return f"eq_{s}" @@ -19,15 +33,6 @@ 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 per_sva(mod: Module, ctx: Context): if ctx == Context.INPUT: return f"{mod.get_hier_path('_')}_input" @@ -52,8 +57,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 @@ -67,6 +71,16 @@ 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 @@ -74,6 +88,8 @@ def __init__(self, topmod: Module) -> None: self.holes: dict[str, PERHole] = {} + self.property_context = SVAContext() + def _generate_decls_for_per(self, per: PER): declbase = per.logic.get_hier_path_nonindex() declfull = per.logic.get_hier_path("_") @@ -189,22 +205,21 @@ 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) - 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 = [] @@ -217,72 +232,130 @@ def generate_decls(self, check_pred: str, 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(!({check_pred}) |-> ({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({check_pred} |-> ({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(!({check_pred}) |-> ({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({check_pred} |-> ({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(!({check_pred}) |-> {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(({check_pred}) |-> {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) + 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"{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"{get_as_prop(TOP_STEP_PROP(i))} : assert property\n" + + 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): # 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_SIGNAL} = ({COUNTER} == {counter_width}'d{k}); """ + for i in range(k): + 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) - 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)) + + 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") @@ -292,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") @@ -300,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") @@ -313,4 +395,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..1c1b7ac 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): @@ -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) - enable_assm_2t(self.psc.context) + 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 950d543..ea893c7 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 @@ -36,17 +38,16 @@ 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) - # Disable all holes in the specification - 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.svagen.property_context) - 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 @@ -73,13 +74,46 @@ 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 - enable_assm_2t(self.psc.context) + set_assm_induction_2t(self.psc.context, self.svagen.property_context) - 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) + # Enable the assumptions for 1 trace verification + 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) + ] + ) + logger.info(f"One trace verification result:\n\t{results_str}") + return results diff --git a/pycmain.py b/pycmain.py index 7d31e36..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 +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,21 +24,55 @@ logger = logging.getLogger(__name__) - -def verif_main(args): - - if args.onetrace: - pconfig, tmgr, module = start(PYCTask.VERIF1T, args) - verifier = JGVerifier1Trace(pconfig) +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.") + 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) - -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) @@ -47,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) @@ -64,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 @@ -89,73 +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="" - ) - - verif.add_argument( - "--onetrace", - help="Verify only one-trace properties.", - 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 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 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 3be8287..781f3cf 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,56 +22,65 @@ import pycaliper.jginterface.jasperclient as jgc from pycaliper.btorinterface.pycbtorsymex import PYCBTORSymex from pycaliper.verif.btorverifier import BTORVerifier2Trace +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.DEBUG) +h1.setLevel(logging.INFO) +h1.setFormatter(logging.Formatter("%(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", -) +h2 = logging.FileHandler("test_debug.log", mode="w") +h2.setLevel(logging.DEBUG) +h2.setFormatter(logging.Formatter("%(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__) 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): @@ -125,5 +134,26 @@ def test_btorverifier1(self): 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) + tmgr.close() + + if __name__ == "__main__": unittest.main()