Enabler-based synchronizer model for clock domain crossing static verification

In the context of industrial size circuits, the interconnection of many blocks from many sources lead to globally asynchronous locally synchronous designs. The transmission of information between clock domains requires complex synchronizers, the correctness of which must be thoroughly verified. Current EDA tools are able to recognize predefined synchronizing modules, but fail to identify custom synchronizers. This paper presents a new model and a set of properties to automatically extract synchronizers in a flat design, and formally verify the correctness of the implemented synchronization protocol.