Dr. Cunxi Yu

Computer Systems Laboratory (CSL), Cornell University

Office: 471 Rhodes Hall

Address:

471 Rhodes Hall
Cornell Univerisity
Ithaca, NY, 14850, USA


Email: cunxi(dot)yu(at)cornell(dot)edu

 

About Me

Cunxi is a Postdoctoral Associate at Cornell University with Prof. Zhiru Zhang. Before joining Cornell, Cunxi was a Postdoctoral Researcher at Integrated Systems Laboratory (LSI) at EPFL, Lausanne, Switzerland, with Prof. Giovanni De Micheli. He received Ph.D degree from University of Massachusetts Amherst (UMass Amherst) in 2017, under the supervision of Prof. Maciej Ciesielski. His research interests focus on applied machine learning, electronic design automation, deep learning, formal verification, and hardware security. His Ph.D. dissertation focuses on formal analysis of arithmetic circuits, including verification, abstraction, and reverse engineering using computer algebra. His thesis was nominated for ACM Outstanding Ph.D dissertation award by UMass. Cunxi spent 11 months as a research intern at IBM T.J Watson Research Center in 2015 and 2016. His work received the best paper nominations at ASP-DAC (2017), TCAD Best paper nomination (2018), and won the 1st place at DAC Security Contest (2017).

Research Interests

Formal Methods, Electronic Design Automation(EDA), Machine Learning, Hardware Security.

Research Employments

  • Postdoctoral Associate, Cornell University (09/2018 - present )
  • Postdoctoral Researcher, EPFL | École polytechnique fédérale de Lausanne, Lausanne, Switzerland (08/2017 - 08/2018 )
  • Research Assistant, University of Massachusetts, Amherst, VLSI CAD Laboratory (01/2014 - 07/2017)
  • Research Intern, IBM Thomas J. Watson Research Center, Yorktown Height, New York, USA ( 05/2016 - 11/2016)
  • Research Intern, IBM Thomas J. Watson Research Center, Yorktown Height, New York, USA ( 05/2015 - 09/2015)

Education

Tools & Datasets

  • De-camouflaging using Incremental SAT [DATE'16] [TCAD'16] [Link]
  • Parallel Analysis of Galois Field Arithmetic - Verification and Reverse Engineering [APS-DAC'17] [DATE'17][TCAD'18] [Link]

Publications

2019

2018

2017

2016

  • Formal Verification of Arithmetic Circuits by Function Extraction. [Tool] [Benchmarks](Best Paper Nomination)
    Cunxi Yu, Walter Brown, Duo Liu, Andre Rossi , Maciej Ciesielski.
    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. (TCAD'16) 10.1109/TCAD.2016.2547898

  • Incremental SAT-based Reverse Engineering of Camouflaged Logic Circuits. [Project Web] [Source code] [Benchmarks]
    Cunxi Yu, Xiangyu Zhang, Duo Liu, Maciej Ciesielski, Daniel Holcomb.
    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. (TCAD'16)

  • Formal Verification using Don’t-care and Vanishing Polynomials.
    Cunxi Yu and Maciej Ciesielski
    2016 IEEE Computer Society Annual Symposium on VLSI (ISVLSI'16) , July 2016, Pittsburgh, PA, USA

  • Analyzing Imprecise Adders using BDDs - A Case Study.
    Cunxi Yu and Maciej Ciesielski
    2016 IEEE Computer Society Annual Symposium on VLSI (ISVLSI'16) , July 2016, Pittsburgh, PA, USA

  • DAG-Aware Logic synthesis of Datapaths (Corrected version).
    Cunxi Yu, Mihir Choudhury, Andrew Sullivan and Maciej Ciesielski
    IEEE/ACM 53rd Design Automation Conference (DAC'16), June 2016, Austin, USA.

  • Automatic Word-level Abstraction on Datapaths.
    Cunxi Yu and Maciej Ciesielski
    IEEE International Symposium on Circuits and System (ISCAS'16) IEEE, May 2016, Montreal, Canada.

  • Oracle-Guided Incremental SAT Solving to Reverse Engineer Camouflaged Logic Circuits.
    Duo Liu, Cunxi Yu and Daniel Holcomb
    IEEE/ACM/EDAA Design, Automation and Test in Europe (DATE'16), March 2016, Dresden, Germany.

2015

  • Logic Debugging of Arithmetic Circuits.
    Samaneh Ghandali, Cunxi Yu, Duo Liu, Maciej Ciesielski
    2015 IEEE Computer Society Annual Symposium on VLSI (ISVLSI'15) , July 2015, Montpellier, France.
  • Verification of Arithmetic Datapath Designs using Word-level Approach.
    Cunxi Yu, Walter. Brown and Maciej. Ciesielski
    2015 IEEE International Symposium on Circuits and Systems (ISCAS). May 2015, Lisbon,Portugal.
  • Verification of Gate-level Arithmetic Circuits by Function Extraction[Tools + Benchmarks]
    Maciej Ciesielski, Cunxi Yu, Walter Brown, Duo Liu and Andre Rossi
    IEEE/ACM 52nd Design Automation Conference (DAC). June, 2015, San Francisco, CA, USA.
  • Diagnosis and Debugging of Arithmetic Circuits
    Samaneh Ghandali, Cunxi Yu, Duo Liu, Maciej Ciesielski
    IEEE/ACM 52nd Design Automation Conference (DAC-WIP). June, 2015, San Francisco, CA, USA.
  • Verification of Sequential Arithmetic Circuit.
    Cunxi Yu, Duo Liu, Walter Brown, Samaneh Ghandali, Maciej Ciesielski
    IEEE/ACM 52nd Design Automation Conference (DAC-WIP). June, 2015, San Francisco, CA, USA.

Teaching

  • Teaching Assistant, ECE 667 (Grad) - Synthesis and Verification of Digital Systems (Spring 2016), UMass Amherst.

  • Teaching Assistant, ECE 597/697 (Grad) - Embedded System (Spring 2015), UMass Amherst

  • Teaching Assistant, ECE 221 (Undergrad) - Introduction to Digital Systems(Fall 2015), UMass Amherst

     

Awards

  • 2017 IWLS Travel Grant

  • 2017 ASP-DAC Best paper nomination
  • 2016 IEEE TVLSI Travel Grant

 

Professional Service

  • TPC Member: IWLS'17, IWLS'18, DUHDe@DATE'19

  • Conference Reviewer: VTS'15, ICCAD'15, CHES'16, DAC'17, DAC'18, ASPDAC'19, FPGA'19

  • Journal Reviewer: IEEE Transactions on VLSI, IEEE Design&Test, IEEE Transactions on CAD, IEEE Transactions on Information Forensics and Security

Presentations

  • Developing Synthesis Flows without Human Knowledge. ACM/IEEE Design Automation Conference (DAC'18). CA, USA. June 2018 (to appear)
  • Approaching Human-Free Synthesis Synthesis for IC Design. Technische Universit├Ąt Kaiserslautern. June 2018.
  • Approaching Human-Free Synthesis Synthesis for IC Design. IBM T.J. Watson Research Center. March. 2018
  • Advanced Datapath Synthesis using Graph Isomorphism. ICCAD 2017, Irvine, CA, USA, November 2017.
  • Reverse Engineering Irreducible Polynomial of GF(2^m) Arithmetic. DATE'2017, Lausanne, Switzerland, March 2017.
  • Efficient Parallel Verification of Galois Field Multipliers. ASP-DAC'17, Japan, Tokyo/Chiba.
  • Computer Algebra Knows Arithmetic Better. École polytechnique fédérale de Lausanne (EPFL). December 2016. Lausanne, Switzerland
  • Formal Analysis of Arithmetic Circuits using Computer Algebra Method. Cadence Conformal LEC. September 2016, Cadence, San Jose, CA, USA.
  • Advanced Datapath Synthesis using Graph Isomorphism. IBM CMOS Design Forum. September 2016, IBM T.J Watson Research Center, Yorktown Height, NY, USA

  • Formal Verification using Don’t-care and Vanishing Polynomials. 2016 IEEE Computer Society Annual Symposium on VLSI (ISVLSI’16) , July 2016, Pittsburgh USA.

  • Analyzing Imprecise Adders using BDDs - A Case Study. 2016 IEEE Computer Society Annual Symposium on VLSI (ISVLSI’16) , July 2016, Pittsburgh USA
  • DAG-Aware Logic synthesis of Datapaths. 53rd Design Automation Conference (DAC’16), June 2016, Austin, USA.
  • Automatic Word-level Abstraction on Datapaths. 2016 IEEE International Symposium on Circuits and System (ISCAS’16) IEEE, May 2016, Montreal
  • Logic Minimization of Multiplexers and the Surrounding Logic. IBM CMOS Design Forum. August 2015, Yorktown Height, NY, USA.
  • Verification of Gate-level Arithmetic Circuits by Function Extraction. 52nd Design Automation Conference (DAC’15), June 2015, San Francisco, USA.