Polynomial Formal Verification of Sequential Circuits

Recently, the concept of Polynomial Formal Verification (PFV) has been introduced and successfully applied to several classes of functions, allowing complete verification under resource constraints. But so far, all studies were carried out for combinational circuits only. In this paper we show how t...

Full description

Saved in:
Bibliographic Details
Main Authors: Dominik, Caroline, Drechsler, Rolf
Format: Conference Proceeding
Language:English
Subjects:
BDD
circuit design
Combinational circuits
correctness
formal methods
Formal verification
Memory management
Polynomials
Sequential circuits
test
Upper bound
verification
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Recently, the concept of Polynomial Formal Verification (PFV) has been introduced and successfully applied to several classes of functions, allowing complete verification under resource constraints. But so far, all studies were carried out for combinational circuits only. In this paper we show how the concept of PFV can be extended to sequential circuits. As a first case study we show for counters that PFV can be performed, even though they have an exponential number of states, i.e., they can be fully formally verified within polynomial upper bounds on run-time and memory requirement.
ISSN:1558-1101
DOI:10.23919/DATE58400.2024.10546775