Title :
Symbolic verification of hardware systems
Author :
Barringer, Howard ; Gough, Graham ; Monahan, Brian ; Williams, Alan
Author_Institution :
Dept. of Comput. Sci., Manchester Univ., UK
fDate :
29 Aug-1 Sep 1995
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;
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
DOI :
10.1109/ASPDAC.1995.486380
