Loading...
Please wait, while we are loading the content...
Similar Documents
Formal Veriication of Pipelined Machines with Out-of-order Execution
| Content Provider | Semantic Scholar |
|---|---|
| Author | Sawada, Jun |
| Copyright Year | 2007 |
| Abstract | This paper discusses the technical details of the design veriication of a pipelined processor with out-of-order execution. We have developed new techniques to verify pipelined processors with complex control logic. Our principal technique is modeling the stream of instructions using a table representation, which allows us to directly express many machine-relevant properties. Using this representation, we have veriied pipeline properties incrementally, and eventually veriied a complete pipelined machine design , whose correctness is deened using the idea of pipeline ushing. The proof has been mechanically checked by ACL2 theorem prover. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.utexas.edu/users/sawada/techreport.ps |
| Alternate Webpage(s) | http://www.cs.utexas.edu/users/boyer/sawada/publication/small-pm.ps |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
