Formal verification of pipelined processors with precise exceptions
| Autor: | R.K. Shyamasundar, K. Kalyanasundaram |
|---|---|
| Rok vydání: | 2005 |
| Předmět: |
Structure (mathematical logic)
Floating point Out-of-order execution Programming language Computer science Pipeline (computing) Parallel computing computer.software_genre Range (mathematics) Automated theorem proving Hardware_REGISTER-TRANSFER-LEVELIMPLEMENTATION computer Formal verification Integer (computer science) |
| Zdroj: | MEMOCODE |
| DOI: | 10.1109/memcod.2004.1459832 |
| Popis: | Verification of pipelined processors is a complex and challenging issue. In this paper, we develop a methodology based on translation validation for the verification of pipelined processors that support precise exceptions and out-of-order executions. We have developed a tool integrated with STeP theorem prover for the automatic verification of pipelined architectures. Formal verification of DLX processor is illustrated using our methodology. It is shown that the precise exception modelling is preserved over a range of pipeline instructions of DLX pipeline, like, integer, floating point, branch instructions, etc. The methodology is also illustrated with examples from DLX processor. A comparative evaluation of our method with other approaches is done and a structure of the tool is also provided. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|