I come from Milan, the financial and fashion capital city of Italy. I got a M.Sc. in electrical engineering in 2008 from Politecnico di Milano, with a thesis on the design of a Time-to-Digital converter for an All-Digital PLL. During my studies, I spent seven months at LTH in Lund, Sweden, as a student enrolled in the Erasmus exchange program. I also graduated from the Alta Scuola Politecnica, a school of excellence in Milan and Turin, with a thesis on robotics for civil applications. As a conclusions of this program, I got a second M.Sc. in electrical engineering from Politecnico di Torino.

From January 2009 to July 2009, I was with ST-Ericsson in Agrate Brianza, as an intern analog IC designer.

From September 2009, I am a Ph.D. student at the University of California - Berkeley in the department of Electrical Engineering and Computer Science. My advisor is professor Sangiovanni-Vincentelli.

• Methodologies for the co-design of analog and digital circuits.
  Effective techniques for the co-design of the analog and digital blocks of SOCs would dramatically decrease the development time of these systems and enable large savings in terms of area and power dissipation.
  My research focuses on devising effective and computational efficient techniques to correctly model the composition of analog and digital blocks, a key step in the exploration of the design space.
• Formal verification techniques for non-linear hybrid systems with continuous dynamics.
  Formal techniques for the verification of systems that exhibit both discrete and continuous dynamics, e.g. AMS circuits, may substantially reduce design costs and time; however, their adoption has been limited by the lack of effective algorithms to capture non-linear behaviors. In an attempt to fill this gap, we developed CalCS, an SMT solver that supports a theory on convex predicates over real valued variables by using results from convex optimization.
• Synthesis and analysis of wireless sensor networks for civil building applications.
  Recent technological advancements have enabled the development of tiny, cheap and power efficient wireless sensors. An increasing interest has been shown in applying this technology to enhance the security, life comfort and power efficiency of civil buildings, mainly because of the huge potential market for these new applications.
  While the design of sensor devices is a fairly mature field, system level design of sensor networks still present several challenges. I am interested in studying computational efficient synthesis and analysis techniques for the design of sensor networks, with specific focus in guaranteeing resilient functionality also in the harsh wireless environment in which these sensors operate.

• Time-to-Digital Converter with 3-ps Resolution and Digital Linearization Algorithm
  M. Zanuso, S. Levantino, A. Puggelli, C. Samori, A. Lacaita; Proceedings of ESSCIRC 2010.

  
  Abstract This paper presents a digital scrambling technique to improve the linearity of flash time-to-digital converters (TDCs) with sub-gate-delay time resolution. Thanks to this approach, a flash TDC using N time arbiters behaves as a quasi-stochastic TDC with an equivalent number of samples equal to N2, at the negligible area cost of doubling the number of minimum load capacitors. The concept is proved in a 65-nm CMOS technology 40MHz TDC, which achieves a 3ps resolution. The differential nonlinearity is reduced from 1LSB to less than 0.2LSB.
  
  
• CalCS: SMT Solving for Non-Linear Convex Constraints
  P. Nuzzo, A. Puggelli, S. A. Seshia, A. Sangiovanni-Vincentelli; Proceedings of FMCAD 2010.

  
  Abstract Certain formal verification tasks require reasoning about Boolean combinations of nonlinear arithmetic constraints over the real numbers. In this paper, we present a new technique for satisfiability solving of Boolean combinations of nonlinear constraints that are convex. Our approach applies fundamental results from the theory of convex programming to realize a satisfiability modulo theory (SMT) solver. Our solver, CalCS, uses a lazy combination of SAT and a theory solver. A key step in our algorithm is the use of complementary slackness and duality theory to generate succinct infeasibility proofs that support conflict-driven learning. Moreover, whenever non-convex constraints are produced from Boolean reasoning, we provide a procedure that generates conservative approximations of the original set of constraints by using geometric properties of convex sets and supporting hyperplanes. We validate CalCS on several benchmarks including formulas generated from bounded model checking of hybrid automata and static analysis of floating-point software.
  
  
• Are Logic Synthesis Tools Robust?
  A. Puggelli, T. Welp, A. Kuehlmann, A. Sangiovanni-Vincentelli; Proceedings of the 48^th Design Automation Conference, June 2011.

  
  Abstract