|
|
|
|
| LEADER |
02938nam a22003257 4500 |
| 001 |
b6743698-e3b2-496e-b7bb-99a23a59c701 |
| 005 |
20240926000000.0 |
| 008 |
951011e199510uuxx |||||||||||||||||eng|| |
| 027 |
1 |
|
|a CS-TR-95-1557
|
| 035 |
|
|
|a (OCoLC-I)728556419
|
| 035 |
|
|
|a (OCoLC-M)728531219
|
| 035 |
|
|
|a (Sirsi) a4639850
|
| 088 |
|
|
|a STANFORD.CS//CS-TR-95-1557
|
| 110 |
2 |
0 |
|a Stanford University
|b Computer Science Department
|n CS-TR-95-1557.
|
| 245 |
1 |
0 |
|a Hierarchical Models of Synchronous Circuits for Formal Verification and Substitution
|
| 260 |
1 |
|
|c October 1995
|
| 300 |
|
|
|a 207 p
|
| 500 |
|
|
|a Bib-Version: CS-TR-v2.0
|
| 500 |
|
|
|a [Adminitrivia V1/Prg/19951011]
|
| 513 |
|
|
|a Technical Report
|
| 513 |
|
|
|a Thesis
|
| 520 |
|
|
|a For hierarchical verification, we model synchronous circuit specifications and implementations uniformly. Each of these descriptions provides both a behavioral and a structural view of the circuit or specification being modeled. We compare the behavior of a circuit model to a requirements specification in order to determine whether the circuit is an acceptable implementation of the specification. Our structural view of a circuit provides the capability to plug in one circuit component in place of another. We derive a requirements specification for the acceptable replacement components, in terms of the desired behavior of the full circuit. We also support nondeterministic specifications, which capture the minimum requirements of a circuit
|
| 520 |
|
|
|a Previous formalisms have relied on syntactic methods for distinguishing apparent from actual unlatched feedback loops in hierarchical hardware designs. However, these methods are not applicable to nondeterministic models. Our model of the behavior of a synchronous circuit within a single clock cycle provides a semantic method to identify cyclic dependencies even in the presence of nondeterminism
|
| 520 |
|
|
|a We develop a mathematical model of synchronous sequential circuits that supports both formal hierarchical verification and substitution. We have implemented and proved the correctness of automatic decision procedures for both of these applications using these models
|
| 700 |
1 |
|
|a Wolf, Elizabeth Susan
|
| 999 |
1 |
0 |
|i b6743698-e3b2-496e-b7bb-99a23a59c701
|l a4639850
|s US-CST
|m hierarchical_models_of_synchronous_circuits_for_formal_verification_an_____1995____________a________________________________________stanford_university________________p
|
| 999 |
1 |
1 |
|l a4639850
|s ISIL:US-CST
|t BKS
|b 472fe74f-6278-501e-9ad1-e0575bf9acdb
|y 472fe74f-6278-501e-9ad1-e0575bf9acdb
|p UNLOANABLE
|
| 999 |
1 |
1 |
|l a4639850
|s ISIL:US-CST
|t BKS
|a SAL3-STACKS
|b 36105018906458
|c 025557
|d Shelving control number
|k 1
|x book
|y 36105018906458
|p UNLOANABLE
|
| 999 |
1 |
1 |
|l a4639850
|s ISIL:US-CST
|t BKS
|a SPEC-SAL3-U-ARCHIVES
|b 36105125029251
|c 025557
|d Shelving control number
|k 1
|x book
|y 36105125029251
|p UNLOANABLE
|
| 999 |
1 |
1 |
|l a4639850
|s ISIL:US-CST
|t BKS
|a SUL-SDR
|p UNLOANABLE
|