| dc.contributor.author | Sarker, Koushik | |
| dc.description.abstract | The constant shrinking of technology has lead to several design challenges that
the synchronous design paradigm is unable to cope with. Elastic design is a novel and
promising design paradigm that overcomes many of these challenges by using
components that are insensitive to the latencies of its inputs.
Verification is a critical problem for any design paradigm. The complexity of
elastic designs arises when the system is pipelined. We develop formal verification
techniques to verify synchronous elastic pipelined systems. Note that the goal of
verification 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.
We develop two formal verification procedures. The first procedure checks the
correctness of elastic pipelined systems against their synchronous parent pipelined
systems. The second procedure checks the correctness of elastic pipelined systems
against their high-level non-pipelined specifications (such as an instruction set
architecture). Datatlow through elastic architectures is complicated by the insertion of
any number of elastic buffers in any place in the design. We introduce elastic tokenflow
diagrams, which arc used to track the flow of data in elastic architectures. We
provide a method to construct such diagrams. We also develop highly automated and
systematic procedures based on elastic token-flow diagrams that compute functions that map states of elastic systems to states of their specifications. Such functions, known as
refinement maps, are used to compare behaviors of elastic and synchronous systems and
hence prove their equivalence. We elasticized a 5-stage DLX processor that enables the
insertion of buffers in its data path. We constructed several elastic processors by
introducing up to 5 elastic buffers at various places in the data path and verified
equivalence with both their synchronous parent pipelined systems and also with their
instruction set architecture specifications. | en_US |
| dc.publisher | North Dakota State University | en_US |
| dc.rights | NDSU policy 190.6.2 | en_US |
| dc.title | Verification of Synchronous Elastic Pipelined Systems | en_US |
| dc.type | Master's Paper | en_US |
| dc.date.accessioned | 2024-01-26T15:40:25Z | |
| dc.date.available | 2024-01-26T15:40:25Z | |
| dc.date.issued | 2010 | |
| dc.identifier.uri | https://hdl.handle.net/10365/33626 | |
| 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 | Electrical and Computer Engineering | en_US |
| ndsu.advisor | Srinivasan, Sudarshan K. | |
