An environment for formal verification based on symbolic computations |
| |
Authors: | Hojati Ramin Brayton Robert K |
| |
Affiliation: | (1) Electrical Engineering and Computer Science, University of California, Berkeley, 94720 Berkeley, CA |
| |
Abstract: | We present an environment for formally verifying hardware, based on symbolic computations. This includes a new concurrency model, called the combinational/sequential or C/S concurrency model which has close ties to hardware. We allow fairness constraints and describe methods for specifying them and for formally verifying in their presence. Properties are specified by either CTL formulae or edge-Rabin automata. We give algorithms, in the presence of fairness constraints, for model checking CTL or for checking that the language of our system is contained in the language of a property automation. Finally, techniques are given for hierarchical verification and for detecting errors quickly (early failure detection). |
| |
Keywords: | Formal verification hardware verification language containment model checking formal specification |
本文献已被 SpringerLink 等数据库收录! |
|