Nel campo della progettazione moderna della CPU il flusso di lavoro di sviluppo vede nei primi passi la descrizione di un modello algoritmico di alto livello da cui i progettisti prenderanno ispirazione per produrre un'implementazione RTL capace di soddisfare idealmente queste specifiche di riferimento i. Potenti tecniche vengono utilizzate oggi per verificare questi CPU designs e la verifica formale fornisce un grande livello di fiducia durante l'analisi sulla correttezza delle nostre implementazioni. Mentre la capacità di descrivere proprietà interessanti scrivendo asserzioni e covers possono essere cruciali per verificare i nostri designs, l'uso delle tecniche formali di equivalenza sembra adeguato all'obiettivo di correlare il modello di riferimento algoritmico con l'implementazione RTL.