A Hierarchical Approach to Self-Timed Circuit Verification
| Autor: | Cuong K. Chau, Warren A. Hunt, Ivan E. Sutherland, Matt Kaufmann, Marly Roncken |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Computer science
Hardware description language Parameterized complexity 020207 software engineering Natural number 02 engineering and technology Extension (predicate logic) ACL2 Computer Science::Hardware Architecture Automated theorem proving Computer Science::Emerging Technologies Asynchronous communication 0202 electrical engineering electronic engineering information engineering Greatest common divisor Arithmetic computer computer.programming_language |
| Zdroj: | ASYNC |
| DOI: | 10.1109/async.2019.00022 |
| Popis: | Self-timed circuits can be modeled in a link-joint style using a formally defined hardware description language. It has previously been shown how functional properties of these models can be formally verified with the ACL2 theorem prover using a scalable, hierarchical method. Here we extend that method to parameterized circuit families that may have loops and non-deterministic outputs. We illustrate this extension with iterative self-timed circuits that calculate the greatest common divisor of two natural numbers, with circuits that perform arbitrated merges non-deterministically, and with circuits that combine both of these. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|