| dc.contributor.author | Cai, Yangwei | |
| dc.description.abstract | This thesis presents a formal verification procedure to check correctness of the synchronous
elastic pipelined system that incorporates early evaluation against its synchronous
parent system. Note that the goal of the verification procedure is not to establish the
correctness of the algorithm for synthesizing elastic circuits, but instead, to find bugs
and formally prove the correctness of elasticized designs with early evaluation. Dataflow
through elastic architectures is complicated by the insertion of any number of elastic buffers
in any place in the design. Elastic token-flow diagrams are introduced, which are used to
track the flow of data in elastic architectures. We provide a method to construct such
diagrams. The thesis also develops a highly automated and systematic procedure based
on elastic token-flow diagrams that compute functions that map states of elastic systems
to states of the synchronous parent systems. Such functions, known as refinement maps,
are used to compare behaviors of elastic and synchronous systems and hence prove their
equivalence. The effectiveness of this method is demonstrated by verifying 8 synchronous
elastic pipelined processor models with early evaluation. | en_US |
| dc.publisher | North Dakota State University | en_US |
| dc.rights | NDSU policy 190.6.2 | en_US |
| dc.title | Refinementbased Verification of Elastic Pipelined System with Early Evaluation | en_US |
| dc.type | Thesis | en_US |
| dc.date.accessioned | 2024-04-05T22:45:09Z | |
| dc.date.available | 2024-04-05T22:45:09Z | |
| dc.date.issued | 2010 | |
| dc.identifier.uri | https://hdl.handle.net/10365/33769 | |
| dc.subject.lcsh | Integrated circuits -- Verification. | en_US |
| dc.subject.lcsh | Synchronous circuits. | en_US |
| dc.subject.lcsh | Computer architecture. | en_US |
| dc.rights.uri | https://www.ndsu.edu/fileadmin/policy/190.pdf | en_US |
| ndsu.degree | Master of Science (MS) | en_US |
| ndsu.college | Engineering | en_US |
| ndsu.department | Electrical and Computer Engineering | en_US |
| ndsu.program | Integrated circuits -- Verification. | en_US |
| ndsu.program | Synchronous circuits. | en_US |
| ndsu.program | Computer architecture. | en_US |
| ndsu.advisor | Srinivasan, Sudarshan | |
