Symbolic verification of hardware systems

Author

Barringer, Howard ; Gough, Graham ; Monahan, Brian ; Williams, Alan

Author_Institution

Dept. of Comput. Sci., Manchester Univ., UK

fYear

1995

fDate

29 Aug-1 Sep 1995

Firstpage

631

Lastpage

636

Abstract

We describe a method for verifying the behavioural equivalence of hardware systems, modelled as deterministic machines, based on the symbolic simulation of the two systems. The state evolution method compares the behaviour of systems at an abstract level, and reduces the problem of checking the behavioural equivalence to one of needing to prove that a set of logical verification conditions are valid. The approach maintains a high degree of automation while offering the possibility of containing the usual growth in complexity of verification, and can be applied to certain systems which have infinite state-spaces

Keywords

equivalence classes; formal verification; logic testing; theorem proving; abstract level; automation; behavioural equivalence; complexity; deterministic machines; hardware design aids; hardware systems; state evolution method; symbolic simulation; symbolic verification; theorem-proving; verification algorithms; Algorithm design and analysis; Automation; Boolean functions; Computational modeling; Computer science; Data structures; Encoding; Explosions; Hardware; Virtual colonoscopy;

fLanguage

English

Publisher

ieee

Conference_Titel

Design Automation Conference, 1995. Proceedings of the ASP-DAC '95/CHDL '95/VLSI '95., IFIP International Conference on Hardware Description Languages. IFIP International Conference on Very Large Scal

Conference_Location

Chiba

Print_ISBN

4-930813-67-0

Type

conf

DOI

10.1109/ASPDAC.1995.486380

Filename

486380