(Mentor Graphics was acquired by Siemens)
R&D for the core backend of SLEC, leading formal equivalence-checking software for digital systems.
• Specifically, the tool performs sequential equivalence checking of C/C++ spec against RTL (hardware model) which the output of HLS (high-level synthesis).
• Implemented algorithms leveraging automated inductive reasoning to optimize, simulate and analyze operator-graph representations of users' designs.
• The work involved dealing with the challenges of implementing scalable verification software, as well as brainstorming theoretical improvements to extract practical value from an equivalence-checker.