Research in Malik Group Flexible and Scalable Equivalence Checking for Accelerator-Rich Architectures Post-Silicon Validation Firmware Verification using Transaction-Level Modeling