PV3 Ponochecks a user-specified property for a transition system

SMT-based model checker

Application domain/field

Type of tool

Model checker

Expected input

Format:

One of the following The authors note that you could also use Verilog, by first using a tool to translate from Verilog to BTOR2 or SMV. The property is represented as an smt-switch formula.

Expected output

UNKNOWN if the result could not be determined, FALSE if the property does not hold, TRUE if the property holds, or ERROR in case of an internal error. When the property does not hold, then Pono will give a witness trace (either in BTOR2 witness format or the VCD standard format)

Internals

Designed with three use cases in mind:
  1. Push-button verification
  2. Expert verification
  3. Model checker development
The user can ask the tool to attempt to prove the property with or without a bound. If the proof attempt failed then the user can ask for a counterexample trace.If the proof attempt succeeded then Pono can return an inductive invariant that implies the property.

Comments

Pono was developed as the next generation of CoSA and was originally named cosa2.
Hardware Model checking

Links

Repository: https://github.com/upscale-project/pono

Related papers

Pono: A Flexible and Extensible SMT-Based Model Checker (CAV '21)

Last publication date

15 July 2021

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.