|M.Sc Student||Verbitsky Dmitry|
|Subject||Automatic Recognition and Verification of Handshake-Based|
|Department||Department of Electrical Engineering||Supervisors||Professor Ran Ginosar|
|Mr. Reuven Dobkin|
|Full Thesis text|
Modern Systems on Chip (SoC) are built of a number of synchronous modules. Those modules are operated by multiple and usually unrelated clocks. In order to ensure safe communication between them synchronizers are required. Being an integrated part of the chip design, synchronizers must be validated. In current research we concentrate on a certain type of synchronizers which are based on handshake mechanism.
The two main verification techniques are structural and formal verification. The structure of handshake-based synchronizers is too complex for structural verification which can't automatically recognize them. On the other hand, formal verification is a more sophisticated technique, which is capable to analyze such constructs, but on account of high computational complexity which complicates their practical use.
We offer a new verification algorithm, which is a combination of structural and formal verification techniques. It applies structural analysis of circuit netlist with parallel check of verification rules.
This method has been applied successfully to various types of handshake synchronizers. It also proved to be successful in identification of corrupted handshake mechanisms.
In addition to synchronizers verification, we propose a new mesochronous synchronizer architecture, named StarSync. It enables low latency and full throughput crossing of clock domain boundaries having same frequency but different phases and supports full back pressure, where the receiver can start and stop accepting words without any data loss. Variable depth buffering is provided, supporting a wide range of short and long range communications and accommodating multi-cycle wire delays. Burst data can also be accommodated thanks to buffering. Dynamic phase shifting due to varying voltage and temperature are mitigated by increasing the separation between write and read pointers. The synchronizer is exposed to metastability risk only during reset. It is suitable for implementation using standard cell design and requires neither delay lines nor other full custom circuits. It is shown that a minimum of four buffer stages are required, in contrast with previous proposals for three stages.