Xiushan (Shaun) Feng

Personal Information

Canadian Citizen with U.S. Green Card living in Austin Texas   E-mail: xiushan.feng at gmail dot com


  • PhD (2006), Master (2003) of Computer Science, University of British Columbia (UBC), Canada.
  • Master of Computer Engineering (2000), Chinese Academy of Sciences (CAS), China.
  • Bachelor of Computer Engineering (1997), Harbin Institute of Technology (HIT), China.

Working Experience

2017.1 – present, Formal Verification Lead, Samsung Semiconductor (SSI) USA

Lead formal verification group for both GPU and CPU designs

2016.1 – 2016.12, Consulting Member of Technical Staff (Sr. Principle) Engineer, Oracle Labs

Lead formal verification efforts and explore other areas of a software/hardware co-design project

2012.10 – 2016.1, Verification Manager, GPU design, Nvidia Corporation

Managing a team for formal verification, semi-formal verification, and verification methodologies for GPU/CPU/SOC designs.

2011.4 – 2012.10, Verification Specialist, Technology Solutions Organization (TSO), Freescale

As a methodologist of verification, I attacked tough issues include but not limited to ESL design and verification, RTL Assertion Based Verification (ABV), low-power design and verification, post-silicon validation, etc. Meanwhile, part of my job was to collaborate with outside academic researchers and EDA vendors to bring new technology into Freescale.

I proposed some novel ideas and developed tools that greatly improved design cycles. Some ideas are prepared as patent disclosures (4 filed, 2+ are in process).

2007 – 2011.4, MTS Design Engineer, Global Logic Analysis Team, IP CAD, AMD

At AMD, I worked on various areas related to RTL and gate logic analysis, such as logic equivalence checking, model checking, low power verification, RTL partition/linting, etc. As a researcher of high level modeling and verification, I wrote formal verification tools (using commercial prove engines or BDDs/SAT techniques) to support circuit design teams.

2003 – 2006, High Level Modeling and Verification (Research Assistant at UBC, Canada)

This PhD research is on Formal Equivalence Checking of Software Specifications vs. Hardware Implementations. I presented several novel approaches and implemented tools to increase the scalability of the verification. As a part of the research, I developed high-level C models and RTL circuits for Intel IA32 instruction length decoders and used them as test cases.

2000 – 2002 Embedded Software Verification ( Research Assistant at UBC, Canada)

It is a part of my master thesis at UBC focusing on Automatic Formal Verification for Scheduled VLIW Code for TI C62x, Fujitsu FR500 VLIW processors. I wrote C++ ISA-level models (cycle-accurate) for DSP processors and applied symbolic simulation techniques to verify different implementations of digital signal processing algorithms.

1998 – 2000, Network Routing (Independent Researcher at Institute of Computing Technology, CAS, China)

I presented my master thesis with "A Dynamic Routing Scheme in Networks", which gives a novel routing scheme for better routing performance and fault-tolerance ability.

1998 – 1999, Task Scheduling for Multi-computers (Research Assistant at Institute of Computing Technology, CAS, China)

I collaborated with a colleague on “Task Scheduling for Multi-computers”. This work gave several task scheduling heuristics for multiple computing nodes. Experiments done on our high-performance clusters showed great improvements.

1998 – 2000, High Speed DSP Board Design (Research Assistant at Institute of Computing Technology, CAS, China)

Our group at ICT designed a PCI-based DSP board (using multiple TI C6x DSPs) to process vast amounts of geographic data.

Programming Languages:

C/C++, Perl, Shell Scripting, TCL, Verilog, SystemVerilog, Assembly(x86, TI C6x, Fujitsu FR500, etc…), JAVA, etc

Assertion Specification Languages:

SVA, PSL, OVL, OVA, etc...

Recent Awards:

  • Peer to Peer Award, Freescale, 2012
  • 4 Patent Awards, Freescale, 2011-2012
  • LoneStar Awards. AMD, 2011, 2010
  • Author Awards, AMD, 2010, 2009
  • Spotlight Awards, AMD, 2010, 2008
  • Patent Awards, AMD, 2008


Vector Sequence Simplification for Circuit Verification,Xiushan Feng, 2009.

6+ applications in progress.

Selected Publications

Verification of Parametrized RTL, Xiushan Feng, Yinfang Lin, and Jay Bhadra. The 12th International Workshop on Microprocessor Test and Verification (MTV), 2011.

Using Model Checking to Prove Constraints of Combinational Equivalence Checking,Xiushan Feng, Joseph Gutierrez, Mel Pratt, Mark Eslinger, Noam Farkash. Design Verification Conference (DVCon), 2010.

Using Backward Symbolic Justification to Constrain Initial State Don't-Cares in Model Checking, Xiushan Feng, Brian McMinn, Richard Bartolotti, Mark Eslinger. The 10th International Workshop on Microprocessor Test and Verification (MTV), 2009.

Early Cutpoint Insertion for High-level Software vs. RTL Formal Combinational Equivalence Verification, Xiushan Feng, Alan J. Hu. Design Automation Conference (DAC), ACM press, 2006.

Embedded software verification using symbolic execution and uninterpreted functions, David Currie, Xiushan Feng, Masahiro Fujita, Alan J. Hu, Mark Kwan, and Sreeranga Rajan. International Journal of Parallel Programming, pages 61--91, Vol.34 No.1. March 2006.

Cutpoints for formal equivalence verification of embedded software, Xiushan Feng, Alan J. Hu, ACM Conference on Embedded Software (EMSOFT), ACM press. 2005

Partitioned model checking from software specifications, Xiushan Feng, Alan J. Hu, and Jin Yang. Asia South Pacific Design Automation Conference (ASPDAC), IEEE Press, 2005.

Automatic Formal Verification for Scheduled VLIW Code, Xiushan Feng, Alan J. Hu. Languages, Compilers, and Tools for Embedded Systems (SCOPES/LCTES), ACM SIGPLAN, 2002.

A Fault Tolerance Routing Scheme in dynamic Networks, Xiushan Feng, Chengde Han, Journal of Computer Science and Technology, P371-380, Vol.16 No.4. 2001

MNLIRS Routing: A Framework for Compressed Routing Table and Fault-tolerant Routing in Networks of Clusters, Xiushan Feng, Chengde Han, The Fourth International Conference on High Performance Computing in Asia-Pacific region, IEEE Press, 2000.

Task Scheduling for Hypercube Interconnected Multicomputers, Jun Zhang, Xiushan Feng, Journal of software, 1999.12