Validating PowerPC microprocessor custom memories

Due to the high cost of correcting errors in a final product, there is a gr owing impetus in industry towards methodologies that can yield correct desi gns in the first manufacturing run. Design validation methodologies that co mbine simulation techniques with formal reasoning can be effective in ensur ing correct operation of software and hardware systems. We show why simulat ion is necessary to complement formal mathematical reasoning in verifying c ertain classes of custom designed circuits. We present a validation methodo logy for PowerPC custom memories based on symbolic simulation.