Alberto PuggelliGraduate Student
| Email: || puggelli(at)eecs.berkeley.edu |
| Address: || 545P Cory Hall |
Berkeley, CA 94720-1770
| Resume: || here |
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. In summer 2011, I interned in Kilby Labs, one of the research centers of Texas Instruments. In summer 2012, I interned again at Texas Instruments, to design an USB/SATA/PCI-e high-speed redriver.
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 advisors are prof. Alberto Sangiovanni-Vincentelli and prof. Elad Alon.
My current research interests mainly focus on 3 topics:
- Automatic design of on-die Switched-Capacitor DCDC converters.
The quest to reduce power consumption of digital systems have risen interest in architectures partitioned in fine-grained voltage and frequency islands to be power-managed independently using on-die DCDC converters. Truly automated low-power synthesis flow will require tools to support also the design of these analog converters. In this project, I aim to automate the design of a switched-capacitor DCDC converter from system specifications to DRC/LVS-free layout. The proposed flow will be validated by prototyping three automatically-designed converters in CMOS 65nm.
- A Design Framework for Distributed Power Management of Heterogeneous Systems-on-Chip.
I am developing a framework to support the design of integrated systems with on-chip distributed power management. Digital circuits are automatically co-designed with the corresponding analog power management units, enabling architectural exploration and evaluation of different control and management policies.
- 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.
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. L. Sangiovanni-Vincentelli; Proceedings of FMCAD 2010.
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
- Are Logic Synthesis Tools Robust?
A. Puggelli, T. Welp, A. Kuehlmann, A. L. Sangiovanni-Vincentelli; Proceedings of the 48th Design Automation Conference, June 2011.
A systematic investigation is presented about the robustness of logic synthesis tools to equivalence-preserving transformations of the input Verilog file. We have developed a framework that (1) parses Verilog behavioral models into an abstract syntax tree, (2) generates random equivalence-preserving transformations on the syntax tree, and (3) writes the transformed design back in Verilog format. The original and the transformed Verilog descriptions are then checked for equivalence and synthesized. Results show that average (peak) improvements in area of 2.5% (11%) and length of the critical path of 4% (13%) are achievable. Indeed these figures are comparable to recent advancements in logic synthesis, signaling a relevant lack of robustness in synthesis tools. This lack of robustness suggests that new synthesis algorithms should be evaluated by measuring the average improvement on several transformed files to assess their real contributions to the quality of the results.
Code to transform Verilog files, presented in the paper "Are Logic Synthesis Tools Robust?" at DAC 2011.
- A Routing-Algorithm-Aware Design Tool for Indoor Wireless Sensor Networks
A. Puggelli, M. Mozumdar, A. L. Sangiovanni-Vincentelli, L. Lavagno; Proceedings of ICNC, February 2012.
We present a design tool to assist the rapid prototyping and deployment of wireless sensor networks for building automation systems. We argue that it is possible to design networks that are more resilient to failures and have longer lifetime, if the behavior of routing algorithms is taken into account at design time. Resiliency can be increased by algorithmically adding redundancy to the network at locations where it can be maximally leveraged by routing algorithms during operation. Lifetime can be increased by placing routers where they are most needed according to the expected data traffic patterns, to improve the quality of the transmission. The network synthesis problem is formulated as an optimization problem: we propose a mixed-integer linear program to solve it exactly, and a polynomial-time heuristic that returns close-to-optimal results in a shorter time.
- Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
A. Puggelli, W. Li, A. L. Sangiovanni-Vincentelli, S. A. Seshia; Proceedings of Computer-Aided Verfication (CAV), July 2013.
We address the problem of verifying Probabilistic Computation Tree
Logic (PCTL) properties of Markov Decision Processes (MDPs) whose state
transition probabilities are only known to lie within uncertainty sets. We first
introduce the model of Convex-MDPs (CMDPs), i.e., MDPs with convex uncertainty
sets. CMDPs generalize Interval-MDPs (IMDPs) by allowing also more
expressive (convex) descriptions of uncertainty. Using results on strong duality
for convex programs, we then present a PCTL verification algorithm for CMDPs,
and prove that it runs in time polynomial in the size of a CMDP for a rich subclass
of convex uncertainty models. This result allows us to lower the previously
known algorithmic complexity upper bound for IMDPs from co-NP to PTIME.
We demonstrate the practical effectiveness of the proposed approach by verifying
a consensus protocol and a dynamic configuration protocol for IPv4 addresses.
- Routing-Aware Design of Indoor Wireless Sensor
Networks Using an Interactive Tool
A. Puggelli, M. Mozumdar, L. Lavagno, A. L. Sangiovanni-Vincentelli; IEEE Systems Journal, December 2013.
In this paper, we present an interactive design tool
that can assist rapid prototyping and deployment of wireless
sensor networks for building automation systems. We argue that
it is possible to design networks that are more resilient to failures
and have longer lifetime if the behavior of routing algorithms is
taken into account at design time. Resiliency can be increased by
algorithmically adding redundancy to the network at locations
where it can be maximally leveraged by routing algorithms
during operation. Lifetime can be increased by placing routers
where they are most needed according to the expected data traffic
patterns, to improve the quality of the transmission. The network
synthesis problem is formulated as an optimization problem. We
propose a mixed-integer linear program to solve it exactly, and
a polynomial-time heuristics that returns close-to-optimal results
in a shorter time. We analyze the performance of the designed
networks by using OPNET simulation. Results show that our tool
can assist designing sensor networks that have high throughput
and consume power efficiently.
Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
LP formulations for the verification of the consensus protocol.
Code implementing the tool for the verification of PCTL properties of MDPs with convex uncertainties.
The folder includes also an extra script that runs the verification of the consensus protocol using the Convex Programming (CP) formulation for the ellipsoidal model of uncertainty, i.e. we verified the protocol with the CP procedure also in the presence of non-linear sources of uncertainty. For more information, see the README file.