TIUP: Effective Processor Verification with Tautology-Induced Universal Properties
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911854355283968 |
|---|---|
| author | Li, Yufeng Ci, Yiwei Yang, Qiusong |
| author_facet | Li, Yufeng Ci, Yiwei Yang, Qiusong |
| contents | Design verification is a complex and costly task, especially for large and intricate processor projects. Formal verification techniques provide advantages by thoroughly examining design behaviors, but they require extensive labor and expertise in property formulation. Recent research focuses on verifying designs using the self-consistency universal property, reducing verification difficulty as it is design-independent. However, the single self-consistency property faces false positives and scalability issues due to exponential state space growth. To tackle these challenges, this paper introduces TIUP, a technique using tautologies as universal properties. We show how TIUP effectively uses tautologies as abstract specifications, covering processor data and control paths. TIUP simplifies and streamlines verification for engineers, enabling efficient formal processor verification. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_17094 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | TIUP: Effective Processor Verification with Tautology-Induced Universal Properties Li, Yufeng Ci, Yiwei Yang, Qiusong Logic in Computer Science Hardware Architecture Systems and Control Design verification is a complex and costly task, especially for large and intricate processor projects. Formal verification techniques provide advantages by thoroughly examining design behaviors, but they require extensive labor and expertise in property formulation. Recent research focuses on verifying designs using the self-consistency universal property, reducing verification difficulty as it is design-independent. However, the single self-consistency property faces false positives and scalability issues due to exponential state space growth. To tackle these challenges, this paper introduces TIUP, a technique using tautologies as universal properties. We show how TIUP effectively uses tautologies as abstract specifications, covering processor data and control paths. TIUP simplifies and streamlines verification for engineers, enabling efficient formal processor verification. |
| title | TIUP: Effective Processor Verification with Tautology-Induced Universal Properties |
| topic | Logic in Computer Science Hardware Architecture Systems and Control |
| url | https://arxiv.org/abs/2404.17094 |