• multipliers and adders give the correct answer based on a particular standard,
• a register-transfer-level (RTL) and gate-level model are equivalent,
• a bus protocol (such as PCI, Amba, or RapidIO) is implemented according to a standard,
• CPUs properly implement their instruction set architectures (ISAs),
• digital signal processors correctly calculate their intended functions, and
• distributed-memory designs maintain cache coherency.
• equivalence of models, such as whether the gate model implements the RTL correctly; and
• properties of models, such as whether a design maintains cache coherency or whether multipliers give the correct result.
Carl Pixley is the manager of design verification at Motorola Semiconductor Products Sector's Architecture and Systems Platforms group. His research interests include formal and semiformal verification, sequential equivalence, and syntheses. Pixley has a BS in mathematics from the University of Omaha, an MS in mathematics from Rutgers, and a PhD in mathematics from the State University of New York at Binghamton. He is a member of the IEEE and the Mathematical Association of America.