pycaliper.verif package

Submodules

pycaliper.verif.btorverifier module

PyCaliper

Author: Adwait Godbole, UC Berkeley

File: verif/btorverifier.py

This module provides classes for verifying BTOR designs using PyCaliper’s verification framework.

For licensing information, please refer to the LICENSE file.

class pycaliper.verif.btorverifier.BTORVerifier1Trace(gui=None)

Bases: PYCBTORInterface

verify(specmodule, des, dc)
Return type:

BTORVerifResult

Perform verification for a single module of the following property:

input_eq && state_eq |-> ##1 output_eq && state_eq

Returns:

is SAFE?

Return type:

bool

class pycaliper.verif.btorverifier.BTORVerifier2Trace(gui=None)

Bases: PYCBTORInterface

verify(specmodule, des, dc)
Return type:

BTORVerifResult

Perform verification for a single module of the following property:

input_eq && state_eq |-> ##1 output_eq && state_eq

Returns:

is SAFE?

Return type:

bool

pycaliper.verif.jgverifier module

class pycaliper.verif.jgverifier.JGVerifier1Trace

Bases: object

One trace property verifier

verify(specmodule, pyconfig)

Verify one trace properties for the given module

Return type:

bool

Parameters:

specmodule (SpecModule) – SpecModule to verify

Returns:

True if the module is safe, False otherwise

Return type:

bool

class pycaliper.verif.jgverifier.JGVerifier1TraceBMC

Bases: object

One trace property verifier with BMC

verify(specmodule, pyconfig, schedule)

Verify one trace properties for the given module

Parameters:

  • specmodule (SpecModule) – SpecModule to verify

  • schedule (str) – Simulation constraints

Returns:

True if the module is safe, False otherwise

Return type:

bool

class pycaliper.verif.jgverifier.JGVerifier2Trace

Bases: object

Two trace property verifier

verify(specmodule, pyconfig)

Verify two trace properties for the given module

Return type:

bool

Parameters:

specmodule (SpecModule) – SpecModule to verify

Returns:

True if the module is safe, False otherwise

Return type:

bool

pycaliper.verif.refinementverifier module

class pycaliper.verif.refinementverifier.FunctionalRefinementMap(mappings)

Bases: RefinementMap

mappings: list[tuple[Logic, Expr]]
class pycaliper.verif.refinementverifier.RefinementMap(mappings)

Bases: object

mappings: list[tuple[Expr, Expr]]
class pycaliper.verif.refinementverifier.RefinementVerifier(slv=<btor2ex.boolectorsolver.BoolectorSolver object>)

Bases: object

check_mm_refinement(mod1, mod2, rmap)

Check module-to-module refinement between two modules under a certain refinement map.

Parameters:

  • mod1 – The first module

  • mod2 – The second module

  • rmap – The refinement map

check_ss_refinement(mod, bs1, bs2, flip_props=False)

Check bounded simulation refinement between two simulation schedules.

Parameters:

  • mod – The module to check refinement for

  • bs1 – The first simulation schedule

  • bs2 – The second simulation schedule

  • flip_props – If True, turn assertions from the first schedule into assumptions

convert_expr_to_btor2(expr, bindinst, step=0)

Convert a PyCaliper expression to a BTOR2 expression

dump_and_wait(assm)
reset()

Module contents