טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentKapschitz Yitschak
SubjectFormal verification of synchronizers
DepartmentDepartment of Electrical Engineering
Supervisor Professor Ran Ginosar


Abstract

Correct operation of synchronizers is verified using formal methods. Existence of synchronization circuits in a System on Chip (SoC) is successfully verified by many modern design verification and synthesis tools. However, their proper operation cannot be verified by such tools and algorithms: Correct operation means the proper transfer of a logical value between mutually asynchronous clock domains, while retaining its integrity and preventing its duplication or loss. Model Checking (MC) is employed in this research in order to achieve this goal.

Two main verification methods are presented. The first method, control verification, is protocol specific. The specification is defined by a Signal Transition Graph (STG), which specifies relative order of transitions of various signals involved in the synchronizer. An algorithm for translation of an STG to MC assertions is presented. These assertions are supplied to a Model Checker for proving proper implementation of the synchronizer.

The second method, data verification, ignores the control mechanism of a verified synchronizer. In this method the assertions are written directly at the level of the goal, and are independent of any rather specific implementation. In other words, the assertions directly reflect the desired properties of any synchronizer: integrity of transferred data, and lack of any duplications and  losses.

Both methods require modeling of two asynchronous clocks. This modeling reflects certain non-determinism in the relative order of active edges of these clocks. In some cases modeled non-determinism may cover a larger space than real non-determinism and define a much wider set of possible scenarios. It is permissible, as long as verification does not fail on false negatives (in scenarios that are impossible in reality).

Another issue is the modeling of synchronization circuits (e.g. two consecutive flip-flops), which also involves certain non-determinism. This behavior is a result of metastability that may happen at the analog circuit level, and which leads to non-deterministic propagation delay of a signal through the synchronization circuit.

These methods were successfully applied to verify a number of synchronizers: several flavors of two-flop synchronizer, FIFO, and a Predictive synchronizer.