Oscillator Verification with Probability One
The work
| Authors | Chao Yan; Mark R. Greenstreet |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2012 |
| Citekey | yan2012oscillator |
Where it appeared
| Published in | Formal Methods in Computer-Aided Design (FMCAD) |
|---|---|
| Publisher | IEEE |
| Pages | 165--172 |
Access
| Free full text | https://www.cs.utexas.edu/~hunt/fmcad/FMCAD12/027.pdf |
|---|
Related
| Distinct from | basin1989verification |
|---|---|
| Distinct from | chen2024fullcustom |
| Distinct from | elshehaby2023susceptibility |
| Distinct from | friedrichs2018metastabilitycontaining |
| Distinct from | fugger2016unfaithful |
| Distinct from | juliato2011fault |
| Distinct from | marino1981general |
| Distinct from | oulkaid2025modeles |
| Distinct from | peng2015extending |
| Distinct from | srinivasu2016carbon |
| Distinct from | winskel1988compositional |
| Distinct from | yan2010formal |
From bibtex.
Abstract
This paper presents the formal verification of startup for a differential ring-oscillator circuit used in industrial designs. Dynamical systems theory shows that any oscillator must have a non-empty failure; however, it is possible to show that these failures only occur with zero probability. To do so, this paper generalizes the "cone argument" initially presented in [1] and proves the soundness of this generalization. This paper also shows how concepts from analog design such as differential operation can be soundly incorporated into the verification to produce simpler models and reduce the complexity of the verification task.
A copy is held
pdf, 1.4 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-15 21:33 UTC |
| Approved by | a person 2026-09-16 09:29 UTC |
Filed under
Cite it as
@inproceedings{yan2012oscillator,
title = {Oscillator Verification with Probability One},
author = {Chao Yan and Mark R. Greenstreet},
year = {2012},
booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},
publisher = {IEEE},
pages = {165--172},
}
This record lives at https://refs.drheap.org/yan2012oscillator/ and will keep doing so.