A Bounded Model Checking Tool for Digital Systems

DSVerifier (Digital Systems Verifier) is a bounded model checker to aid enginners to check for overflow, limit cycle, error, timing, stability, and minimum phase in digital systems, considering finite word length (FWL) effects.
Overflow

Ensures the absence of overflows in digital systems implementations.

Limit Cycle

Checks for the presence of persistent undesired oscillations in the output of the digital systems, caused by the finite precision.

Error

Ensures that the output error in digital systems implementation will be within admissible range, considering the FWL effects.

Timing

Checks whether the embedded software of the digital system meets time constraints due to hardware limitations.

Stability

Checks for the stability of the digital systems, considering the FWL effects.

Robust Closed-loop Stability

Checks for the stability of the digital systems in closed-loop considering the FWL effects and uncertainty parameters.

Minimum Phase

Checks whether the digital systems present minimum phase, considering the FWL effects.

About Us

DSVerifier is developed at the Federal University of Amazonas (UFAM). This project is supported by Samsung, CNPq, and FAPEAM grants.
Bounded Model Checking Tool for Digital Systems
  • DSVerifier - Digital Systems Verifier

    DSVerifier (Digital Systems Verifier) is a bounded model checker to aid enginners to check for overflow, limit cycle, error, timing, stability, and minimum phase in digital systems, considering finite word length (FWL) effects.

  • ESBMC - Efficient SMT-Based Context-Bounded Model Checker

    ESBMC is a context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver. It allows the verification engineer to verify single- and multi-threaded software (with shared variables and locks); to reason about arithmetic under- and overflow, pointer safety, memory leaks, array bounds, atomicity and order violations, deadlock and data race; to verify programs that make use of bit-level, pointers, structs, unions and fixed-point arithmetic.

    http://www.esbmc.org
  • Contributors

    • Eddie de Lima Filho • Felipe Monteiro • Hussama Ismail • Iury Bessa • João Edgar Chaves Filho • Lennon C. Chaves • Lucas Cordeiro • Mauro Freitas • Mikhail Ramalho • Renato Abreu • Waldir Sabino Jr.

Federal University of Amazonas, Manaus, Amazonas, Brazil
iury.bessa@gmail.com
hussamaismail@gmail.com
lucasccordeiro@gmail.com