Projectagon-based reachability analysis for circuit-level formal verification
Notice bibliographique
Résumé
This dissertation presents a novel verification technique for analog and mixed signal circuits. Analog circuits are widely used in many applications include consumer electronics, telecommunications, medical electronics. Furthermore, in deep sub-micron design, physical effects might undermine common digital abstractions of circuit behavior. Therefore, it is necessary to develop systematic methodologies to formally verify hardware design using circuit-level models. We present a formal method for circuit-level verification. Our approach is based on translating verification problems to reachability analysis problems. It applies nonlinear ODEs to model circuit dynamics using modified nodal analysis. Forward reachable regions are computed from given initial states to explore all possible circuit behaviors. Analog properties are checked on all circuit states to ensure full correctness or find a design flaw. Our specification language extends LTL logic with continuous time and values and applies Brockett’s annuli to specify analog signals. We also introduced probability into the specification to support practical analog properties such as metastability behavior. We developed and implemented a reachability analysis tool COHO for a simple class of moderate-dimensional hybrid systems with nonlinear ODE dynamics. COHO employs projectagons to represent and manipulate moderate-dimensional, non-convex reachable regions. COHO solves nonlinear ODEs by conservatively approximating ODEs as linear differential inclusions. COHO is robust and efficient. It uses arbitrary precision rational numbers to implement exact computation and trims projectagons to remove infeasible regions. To improve performance and reduce error, several techniques are developed, including a guess-verify strategy, hybrid computation, approximate algorithms, and so on. The correctness and efficiency of our methods have been demonstrated by the success of verifying several circuits, including a toggle circuit, a flip-flop circuit, an arbiter circuit, and a ring-oscillator circuit proposed by researchers from Rambus Inc. Several important properties of these circuits have been verified and a design flaw was spotted during the toggle verification. During the reachability computation, we recognized new problems (e.g., stiffness) and proposed our solutions to these problems. We also developed new methods to analyze complex properties such as metastable behaviors. The combination of these methods and reachability analysis is capable of verifying practical circuits.
Récupéré en direct depuis OpenAlex et désinversé. Les résumés ne sont pas conservés dans cette base de données : les index inversés représentent 8,6 Go des 9,3 Go de texte de la base, et le serveur dispose de 13 Go libres.
Comment cette classification a été obtenuedéplier
Prédiction distillée sur la base complète
Imitation des enseignantsNi prévalence calibrée, ni vérité terrain. Validation humaine à venir. Apprise à partir de 10 348 étiquettes directes de Codex et de 10 348 étiquettes directes de Gemma. Le mode candidate est l'union des têtes enseignantes seuillées; le consensus est leur intersection. Ces sorties portent le statut machine_predicted_unvalidated et ne sont ni des étiquettes humaines ni des étiquettes directes de modèles de pointe.
Scores Codex et Gemma par catégorie
| Catégorie | Codex | Gemma |
|---|---|---|
| Métarecherche | 0,001 | 0,000 |
| Méta-épidémiologie (sens strict) | 0,000 | 0,000 |
| Méta-épidémiologie (sens large) | 0,000 | 0,000 |
| Bibliométrie | 0,000 | 0,001 |
| Études des sciences et des technologies | 0,000 | 0,000 |
| Communication savante | 0,000 | 0,001 |
| Science ouverte | 0,001 | 0,000 |
| Intégrité de la recherche | 0,000 | 0,000 |
| Charge utile insuffisante (le modèle a refusé de juger) | 0,000 | 0,000 |
Scores machine (provisoires)
Les deux têtes enseignantes du modèle étudiant, lues sur ce travail. Un score ordonne la base pour la relecture; il n'affirme jamais une catégorie, et le statut de validation accompagne chaque rangée tel quel.
Scores de référence d'un modèle non mature (critères de maturité non atteints, 7 itérations). Un score ordonne; il n'affirme jamais une catégorie.
score_only:v0-immature-baseline · tel quel depuis la passe de notation : score_only signifie que le nombre peut ordonner les travaux, et qu'aucune étiquette de catégorie n'en découleClassification
machine, non validéePrédiction automatique; un appel candidat d’une seule tête enseignante, pas un consensus.
Le détail, modèle par modèle et score par score, se trouve en fin de page sous « Comment cette classification a été obtenue ».