pycaliper package

Subpackages

Submodules

pycaliper.proofmanager module

class pycaliper.proofmanager.MMRefinementPR(result, spec1, spec2, rmap)

Bases: ProofResult

rmap: RefinementMap
spec1: str
spec2: str
class pycaliper.proofmanager.OneTraceBndPR(result, spec, sched, design)

Bases: ProofResult

design: str
sched: str
spec: str
class pycaliper.proofmanager.OneTraceIndPR(result, spec, design, dc)

Bases: ProofResult

dc: DesignConfig
design: str
spec: str
class pycaliper.proofmanager.ProofManager(webgui=False, cligui=False)

Bases: object

check_mm_refinement(spec1, spec2, rmap)
check_ss_refinement(spec, sched1, sched2, flip=False)

Check if bounded schedule sched1 refines sched2. If flip is True, then the assertions are flipped in sched1.

Return type:

ProofResult

Parameters:

  • spec (SpecModule | str) – The spec to use.

  • sched1 (Callable | str) – The first schedule to check.

  • sched2 (Callable | str) – The second schedule to check.

  • flip (bool, optional) – Flip the assertions in sched1. Defaults to False.

mk_btor_design_from_file(file, name)
Return type:

BTORDesign

mk_btor_proof_one_trace(spec, design, dc=DesignConfig(cpy1='a', cpy2='b', lang='sv12', topmod='', clk='clk'))
Return type:

ProofResult

mk_jg_design_from_pyc(name, pyc)
Return type:

Design

mk_jg_proof_bounded_spec(spec, design, sched)
Return type:

ProofResult

mk_spec(spec, name, **kwargs)
class pycaliper.proofmanager.ProofResult(result)

Bases: object

result: bool
class pycaliper.proofmanager.SSRefinementPR(result, spec, sched1, sched2, flip)

Bases: ProofResult

flip: bool
sched1: str
sched2: str
spec: str
class pycaliper.proofmanager.TwoTraceIndPR(result, spec, design, dc)

Bases: ProofResult

dc: DesignConfig
design: str
spec: str
pycaliper.proofmanager.mk_btordesign(name, filename)

pycaliper.propns module

Namespace for properties

pycaliper.propns.TOP_STEP_PROP(fn_name, k)

Get the property name for a given step

Return type:

str

pycaliper.propns.condeq_sva(s)
pycaliper.propns.eq_sva(s)
pycaliper.propns.get_as_assm(prop)

Get the assumption name for a given property

Return type:

str

pycaliper.propns.get_as_prop(prop)

Get the assertion name for a given property

Return type:

str

pycaliper.pycconfig module

class pycaliper.pycconfig.Design(name)

Bases: object

Base class for design representations.

This class serves as a base for different design representations in PyCaliper.

name

Name of the design.

Type:

str

class pycaliper.pycconfig.DesignConfig(**data)

Bases: BaseModel

Configuration for design verification.

This class holds configuration parameters for design verification.

cpy1

Hierarchy prefix for the first copy of the design.

Type:

str

cpy2

Hierarchy prefix for the second copy of the design.

Type:

str

lang

Hardware description language used for the design.

Type:

str

topmod

Name of the top module in the design.

Type:

str

clk

Name of the clock signal in the design.

Type:

str

clk: str
cpy1: str
cpy2: str
lang: str
model_computed_fields: ClassVar[Dict[str, ComputedFieldInfo]] = {}

A dictionary of computed field names and their corresponding ComputedFieldInfo objects.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

model_fields: ClassVar[Dict[str, FieldInfo]] = {'clk': FieldInfo(annotation=str, required=False, default='clk'), 'cpy1': FieldInfo(annotation=str, required=False, default='a'), 'cpy2': FieldInfo(annotation=str, required=False, default='b'), 'lang': FieldInfo(annotation=str, required=False, default='sv12'), 'topmod': FieldInfo(annotation=str, required=False, default='')}

Metadata about the fields defined on the model, mapping of field names to [FieldInfo][pydantic.fields.FieldInfo] objects.

This replaces Model.__fields__ from Pydantic V1.

topmod: str
class pycaliper.pycconfig.JasperConfig(**data)

Bases: BaseModel

Configuration for Jasper Gold formal verification tool.

This class holds configuration parameters for interacting with the Jasper Gold formal verification tool.

jdir

Jasper working directory relative to the pycaliper directory.

Type:

str

script

TCL script relative to the Jasper working directory.

Type:

str

pycfile

Location of the generated SVA file relative to the Jasper working directory.

Type:

str

context

Proof node context.

Type:

str

design_list

Design list file.

Type:

str

port

Port number to connect to Jasper server.

Type:

int

context: str
design_list: str
jdir: str
model_computed_fields: ClassVar[Dict[str, ComputedFieldInfo]] = {}

A dictionary of computed field names and their corresponding ComputedFieldInfo objects.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

model_fields: ClassVar[Dict[str, FieldInfo]] = {'context': FieldInfo(annotation=str, required=False, default=''), 'design_list': FieldInfo(annotation=str, required=False, default='design.lst'), 'jdir': FieldInfo(annotation=str, required=False, default=''), 'port': FieldInfo(annotation=int, required=False, default=8080), 'pycfile': FieldInfo(annotation=str, required=False, default=''), 'script': FieldInfo(annotation=str, required=False, default='')}

Metadata about the fields defined on the model, mapping of field names to [FieldInfo][pydantic.fields.FieldInfo] objects.

This replaces Model.__fields__ from Pydantic V1.

port: int
pycfile: str
pycfile_abspath()

Get the absolute path to the PyCaliper specification file.

Returns:

Absolute path to the PyCaliper specification file.

Return type:

str

script: str
class pycaliper.pycconfig.PYConfig(**data)

Bases: BaseModel

PyCaliper configuration class.

This class holds the main configuration for PyCaliper tasks.

sdir

Directory to save results to.

Type:

str

mock

Whether to run in mock mode without Jasper access.

Type:

bool

jgc

Jasper configuration.

Type:

JasperConfig

pycspec

Name of the PyCaliper specification.

Type:

str

onetrace

Whether to verify only one-trace properties.

Type:

bool

tdir

Directory containing VCD trace files.

Type:

str

dc

Design configuration.

Type:

DesignConfig

dc: DesignConfig
jgc: JasperConfig
mock: bool
model_computed_fields: ClassVar[Dict[str, ComputedFieldInfo]] = {}

A dictionary of computed field names and their corresponding ComputedFieldInfo objects.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

model_fields: ClassVar[Dict[str, FieldInfo]] = {'dc': FieldInfo(annotation=DesignConfig, required=False, default=DesignConfig(cpy1='a', cpy2='b', lang='sv12', topmod='', clk='clk')), 'jgc': FieldInfo(annotation=JasperConfig, required=False, default=JasperConfig(jdir='', script='', pycfile='', context='', design_list='design.lst', port=8080)), 'mock': FieldInfo(annotation=bool, required=False, default=False), 'onetrace': FieldInfo(annotation=bool, required=False, default=False), 'pycspec': FieldInfo(annotation=str, required=False, default=''), 'sdir': FieldInfo(annotation=str, required=False, default=''), 'tdir': FieldInfo(annotation=str, required=False, default='')}

Metadata about the fields defined on the model, mapping of field names to [FieldInfo][pydantic.fields.FieldInfo] objects.

This replaces Model.__fields__ from Pydantic V1.

onetrace: bool
pycspec: str
sdir: str
tdir: str

pycaliper.pycgui module

class pycaliper.pycgui.GUIPacket(t, iden='', dname='', sname='', file='', params='', proofterm='', result='')

Bases: object

class T

Bases: object

NEW_DESIGN = 0
NEW_PROOF = 2
NEW_SPEC = 1
dname: str = ''
file: str = ''
iden: str = ''
params: str = ''
proofterm: str = ''
result: str = ''
sname: str = ''
t: T
class pycaliper.pycgui.PYCGUI

Bases: object

push_update(data)
reset_progress()
run(debug=True)
update_progress(desc, progress)
class pycaliper.pycgui.RichGUI

Bases: PYCGUI

mk_window()
push_update(data)
reset_progress()
run(debug=True)

Run the Flask-SocketIO server in its own thread so it doesn’t block the main application logic.

update_progress(desc, progress)
class pycaliper.pycgui.WebGUI

Bases: PYCGUI

push_update(data)
reset_progress()
run(debug=True)

Run the Flask-SocketIO server in its own thread so it doesn’t block the main application logic.

update_progress(desc, progress)

pycaliper.pycmain module

pycaliper.pycmain.main()

Main entry point for the PyCaliper command-line interface.

This function initializes and runs the Typer application that provides the command-line interface for PyCaliper.

pycaliper.pycmain.persynth_main(specpath='', jgcpath='', dcpath='', params='', sdir='', strategy='seq', fuelbudget=3, retries=1, stepbudget=10)

Synthesize invariants using Partial Equivalence Relations (PER).

This function performs synthesis of invariants for a PyCaliper specification using the PER synthesis approach. It supports different synthesis strategies and configurable parameters for the synthesis process.

Parameters:

  • specpath (str) – Path to the PyCaliper specification class.

  • jgcpath (str) – Path to the Jasper configuration file.

  • dcpath (str) – Path to the design configuration file.

  • params (str) – Parameters for the specification module in the format key=value.

  • sdir (str) – Directory to save synthesis results to.

  • strategy (str) – Strategy to use for synthesis (‘seq’, ‘rand’, or ‘llm’).

  • fuelbudget (int) – Fuel budget for the synthesis strategy.

  • retries (int) – Number of retries for synthesis.

  • stepbudget (int) – Step budget for synthesis.

pycaliper.pycmain.svagen_main(specpath='', jgcpath='', dcpath='', params='', sdir='')

Generate SystemVerilog Assertions (SVA) from a PyCaliper specification.

This function generates SVA specifications from a PyCaliper specification class. The generated SVA can be used for formal verification in SystemVerilog environments.

Parameters:

  • specpath (str) – Path to the PyCaliper specification class.

  • jgcpath (str) – Path to the Jasper configuration file.

  • dcpath (str) – Path to the design configuration file.

  • params (str) – Parameters for the specification module in the format key=value.

  • sdir (str) – Directory to save the generated SVA file to.

pycaliper.pycmain.verif_main(specpath='', jgcpath='', dcpath='', params='', sdir='', onetrace=False, bmc='')

Verify invariants in a PyCaliper specification.

This function performs formal verification of the properties specified in a PyCaliper specification class. It can perform either one-trace or two-trace verification, and supports bounded model checking.

Parameters:

  • specpath (str) – Path to the PyCaliper specification class.

  • jgcpath (str) – Path to the Jasper configuration file.

  • dcpath (str) – Path to the design configuration file.

  • params (str) – Parameters for the specification module in the format key=value.

  • sdir (str) – Directory to save verification results to.

  • onetrace (bool) – If True, verify only one-trace properties.

  • bmc (str) – If provided, perform verification with bounded model checking.

pycaliper.pycmanager module

class pycaliper.pycmanager.PYCArgs(**data)

Bases: BaseModel

Arguments for PyCaliper tasks.

This class defines the arguments that can be passed to PyCaliper tasks. It uses Pydantic for validation and default values.

specpath

Path to the specification module.

Type:

str

jgcpath

Path to the Jasper configuration file.

Type:

str

dcpath

Path to the design configuration file.

Type:

str

params

Parameters for the specification module.

Type:

str

sdir

Directory to save results to.

Type:

str

tdir

Directory containing trace files.

Type:

str

onetrace

Whether to verify only one-trace properties.

Type:

bool

bmc

Bounded model checking configuration.

Type:

str

bmc: str

Bounded model checking configuration

dcpath: str

Path to the design configuration file

jgcpath: str

Path to the Jasper configuration file

model_computed_fields: ClassVar[Dict[str, ComputedFieldInfo]] = {}

A dictionary of computed field names and their corresponding ComputedFieldInfo objects.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

model_fields: ClassVar[Dict[str, FieldInfo]] = {'bmc': FieldInfo(annotation=str, required=False, default=''), 'dcpath': FieldInfo(annotation=str, required=False, default=''), 'jgcpath': FieldInfo(annotation=str, required=False, default=''), 'onetrace': FieldInfo(annotation=bool, required=False, default=False), 'params': FieldInfo(annotation=str, required=False, default=''), 'sdir': FieldInfo(annotation=str, required=False, default=''), 'specpath': FieldInfo(annotation=str, required=False, default=''), 'tdir': FieldInfo(annotation=str, required=False, default='')}

Metadata about the fields defined on the model, mapping of field names to [FieldInfo][pydantic.fields.FieldInfo] objects.

This replaces Model.__fields__ from Pydantic V1.

onetrace: bool

Whether to verify only one-trace properties

params: str

Parameters for the specification module

sdir: str

Directory to save results to

specpath: str

Path to the specification module

tdir: str

Directory containing trace files

class pycaliper.pycmanager.PYCManager(pyconfig)

Bases: object

Manager for PyCaliper tasks.

This class manages the execution of PyCaliper tasks, including handling of temporary directories, trace files, and specification files.

pycspec

Name of the PyCaliper specification.

Type:

str

pyconfig

Configuration for the PyCaliper task.

Type:

PYConfig

sdir

Directory to save results to.

Type:

str

wdir

Working directory for the task.

Type:

str

tracedir

Directory for trace files.

Type:

str

specdir

Directory for specification files.

Type:

str

num_vcd_files

Number of VCD trace files.

Type:

int

traces

Dictionary of trace file paths.

Type:

dict

num_spec_files

Number of specification files.

Type:

int

specs

Dictionary of specification file paths.

Type:

dict

close()

Close the PyCaliper manager.

This function saves the results and closes the Jasper socket.

create_vcd_path()

Create a new path for a VCD trace file.

Returns:

Path to the new VCD trace file.

Return type:

str

gather_all_traces(tdir)

Gather all VCD trace files from a directory.

This function collects all VCD files in the specified directory and copies them to the trace directory.

Parameters:

tdir (str) – Directory containing VCD trace files.

get_vcd_path(idx)

Get the path to a VCD trace file by index.

Parameters:

idx (int) – Index of the VCD trace file.

Returns:

Path to the VCD trace file.

Return type:

str

get_vcd_path_random()

Get the path to a random VCD trace file.

Returns:

Path to a random VCD trace file, or None if no trace files are available.

Return type:

str

save()

Save the results of the PyCaliper task.

This function copies the contents of the working directory to the specified save directory.

save_spec(module)

Save a specification module to a file.

Parameters:

module (SpecModule) – Specification module to save.

class pycaliper.pycmanager.PYCTask(value)

Bases: Enum

Enumeration of PyCaliper tasks.

Defines the different types of tasks that can be performed by PyCaliper.

CTRLSYNTH = 4

Control synthesis

FULLSYNTH = 6

Full synthesis

PERSYNTH = 5

PER synthesis

SVAGEN = 0

Generate SVA specifications

VERIF1T = 1

One-trace verification

VERIF2T = 2

Two-trace verification

VERIFBMC = 3

Bounded model checking verification

pycaliper.pycmanager.create_module(specpath, args)

Dynamically import the spec module and create an instance of it.

pycaliper.pycmanager.get_pyconfig(args)

Create a PyCaliper configuration from arguments.

This function creates a PyCaliper configuration from the provided arguments, including loading and validating Jasper and design configurations.

Return type:

PYConfig

Parameters:

args (PYCArgs) – PyCaliper arguments.

Returns:

PyCaliper configuration.

Return type:

PYConfig

pycaliper.pycmanager.get_specmodname(specmod)

Extract the specification module name from a path.

Parameters:

specmod (str) – Path to the specification module.

Returns:

Name of the specification module.

Return type:

str

pycaliper.pycmanager.mock_or_connect(pyconfig)

Connect to Jasper or run in mock mode.

Return type:

bool

Parameters:

pyconfig (PYConfig) – PyCaliper configuration.

Returns:

True if connected to Jasper, False if running in mock mode.

Return type:

bool

pycaliper.pycmanager.setup_all(args)

Set up all components for a PyCaliper task.

This function creates a PyCaliper configuration, manager, and connects to Jasper.

Return type:

tuple[bool, PYConfig, PYCManager]

Parameters:

args (PYCArgs) – PyCaliper arguments.

Returns:

Tuple of (is_connected, pyconfig, tmgr).

Return type:

tuple

pycaliper.pycmanager.start(task, args)

Start a PyCaliper task.

This function sets up all components for a PyCaliper task and checks that the task can be run in the current mode.

Return type:

tuple[PYConfig, PYCManager, SpecModule]

Parameters:

  • task (PYCTask) – PyCaliper task to run.

  • args (PYCArgs) – PyCaliper arguments.

Returns:

Tuple of (pyconfig, tmgr, module).

Return type:

tuple

pycaliper.svagen module

Generate SVA (wires, assumes, asserts) for specifications in PER

class pycaliper.svagen.ModuleSpec(**data)

Bases: BaseModel

input_inv_spec_decl_comp: str
input_inv_spec_decl_single: str
input_spec_decl: str
model_computed_fields: ClassVar[Dict[str, ComputedFieldInfo]] = {}

A dictionary of computed field names and their corresponding ComputedFieldInfo objects.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

model_fields: ClassVar[Dict[str, FieldInfo]] = {'input_inv_spec_decl_comp': FieldInfo(annotation=str, required=True), 'input_inv_spec_decl_single': FieldInfo(annotation=str, required=True), 'input_spec_decl': FieldInfo(annotation=str, required=True), 'output_inv_spec_decl_comp': FieldInfo(annotation=str, required=True), 'output_inv_spec_decl_single': FieldInfo(annotation=str, required=True), 'output_spec_decl': FieldInfo(annotation=str, required=True), 'path': FieldInfo(annotation=Path, required=True), 'state_inv_spec_decl_comp': FieldInfo(annotation=str, required=True), 'state_inv_spec_decl_single': FieldInfo(annotation=str, required=True), 'state_spec_decl': FieldInfo(annotation=str, required=True)}

Metadata about the fields defined on the model, mapping of field names to [FieldInfo][pydantic.fields.FieldInfo] objects.

This replaces Model.__fields__ from Pydantic V1.

output_inv_spec_decl_comp: str
output_inv_spec_decl_single: str
output_spec_decl: str
path: Path
state_inv_spec_decl_comp: str
state_inv_spec_decl_single: str
state_spec_decl: str
class pycaliper.svagen.SVAContext(**data)

Bases: BaseModel

asrts_1trace: list[str]
asrts_2trace: list[str]
asrts_bmc: dict[str, list[str]]
assms_1trace: list[str]
assms_2trace: list[str]
assms_bmc: dict[str, list[str]]
holes: list[str]
model_computed_fields: ClassVar[Dict[str, ComputedFieldInfo]] = {}

A dictionary of computed field names and their corresponding ComputedFieldInfo objects.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

model_fields: ClassVar[Dict[str, FieldInfo]] = {'asrts_1trace': FieldInfo(annotation=list[str], required=False, default=[]), 'asrts_2trace': FieldInfo(annotation=list[str], required=False, default=[]), 'asrts_bmc': FieldInfo(annotation=dict[str, list[str]], required=False, default={}), 'assms_1trace': FieldInfo(annotation=list[str], required=False, default=[]), 'assms_2trace': FieldInfo(annotation=list[str], required=False, default=[]), 'assms_bmc': FieldInfo(annotation=dict[str, list[str]], required=False, default={}), 'holes': FieldInfo(annotation=list[str], required=False, default=[])}

Metadata about the fields defined on the model, mapping of field names to [FieldInfo][pydantic.fields.FieldInfo] objects.

This replaces Model.__fields__ from Pydantic V1.

class pycaliper.svagen.SVAGen

Bases: object

counter_step(kd, td)

Generate counter and step signals for the simulation.

Parameters:

  • kd (int) – Number of steps for inductions (generate induction trigger)

  • td (int) – Number of steps across all simulations schedules + induction

create_pyc_specfile(topmod, dc, filename='temp.pyc.sv', onetrace=False)
pycaliper.svagen.inv_sva(mod, spec_ctx)
pycaliper.svagen.per_sva(mod, spec_ctx)
pycaliper.svagen.step_signal(k)

pycaliper.vcdutils module

PyCaliper

Author: Adwait Godbole, UC Berkeley

File: vcdutils.py

Utilities to read VCD files

class pycaliper.vcdutils.Assignment(*args, **kwargs)

Bases: MutableMapping

Assignment map from signals and values in the simulation

class pycaliper.vcdutils.StateValue(val, isx=False)

Bases: object

isx: bool = False
val: int
pycaliper.vcdutils.autodetect_clock(vcdr)

Find the clock signal in the VCD file

Return type:

str

Parameters:

vcdr (VCDVCD) – VCDVCD object read from vcd file

Returns:

clock signal name

Return type:

str

pycaliper.vcdutils.autodetect_clockdelta(vcdr, clk)

Find the clock signal delta in the VCD file

Return type:

int

Parameters:

vcdr (VCDVCD) – VCDVCD object read from vcd file

Returns:

clock timedelta

Return type:

int

pycaliper.vcdutils.get_subtrace(vcdr, sigs, rng, clk, ctx='')
Return type:

list[Assignment]

Extract the signals from the vcd trace between the start_cyc and end_cyc (both inclusive)

This is done only for signals that have counterparts in the design (CSIGs and DSIGs)

Parameters:

  • vcdr (VCDVCD) – VCDVCD object read from vcd file

  • sigs (list[Logic]) – list of Logic signals

  • rng (range) – range denoting the time steps to be sampled at

  • ctx (str, optional) – context string (path to top module). Defaults to ‘’.

Returns:

a list of Assignment objects, one for each step in rng

Return type:

list[Assignment]

pycaliper.vcdutils.get_subtrace_simple(vcdr, sigs, rng)

Extract signal values from the VCD trace directly from the signal names.

Parameters:

  • vcdr (VCDVCD) – VCDVCD object read from vcd file

  • sigs (List[str]) – list of signal names to read from the vcd file

  • rng (range) – range denoting the time steps to be sampled at

Returns:

a list of dictionaries,

representing the memory values at each point

Return type:

List[Dict[str, Union[int, str]]]

pycaliper.vcdutils.signalstr_to_vcdid(sig)

Convert a signal string to a VCD string

Parameters:

sig (str) – signal string

Returns:

VCD string

Return type:

str

Module contents