The jasper_model_async_cdc_wire Proof Accelerator™ (PA) is an encrypted macro to model the effects of metastability and nondeterminism on asynchronous clock domain crossings (CDCs) in a design under verification (DUV). This modeling allows you to prove the functional correctness of your design even for cases where non-deterministic sampling of values between clock domains potentially causes problems. The PA is instantiated at the points where signals cross the clock domain boundaries and enables end-to-end (input to output) formal verification of your properties under all potential phase jitter conditions of completely asynchronous clocks.