Abstract: Nanoscale CMOS technologies keep shrinking the operating voltage while reducing the cost per digital gate. In this scenario, the design of phase-locked loops is evolving from the traditional analog approach to the digital one, and the typical off-chip loop filter is being replaced by an on-chip digital one. This alternative design methodology is also enabling the application of more and more sophisticated digital calibration algorithms to on-the-fly correct the analog impairments and improve frequency agility and jitter performance, paving the way towards new exciting research opportunities.
Biography: Salvatore Levantino is a Full Professor of Electrical Engineering at the Politecnico di Milano, Milan, Italy. He has coauthored Integrated Frequency Synthesizers for Wireless Systems (Cambridge University Press, 2007). He has been a TPC Member of several IEEE conferences such as ISSCC, ESSCIRC, ICECS and RFIC Symposium. He was Guest Editor of the IEEE JSSC, and Associate Editor of the IEEE TCAS-I and TCAS-II. He was a co-recipient of the Best Paper Award of the 2018 ISCAS conference, and was Distinguished Lecturer for the IEEE Solid-State Circuits Society (SSCS).
Authors of paper: Rolf Drechsler, Alireza Mahzoon
With the growing complexity of digital circuits, formal verification has become a crucial task after the design in order to ensure the correctness of a circuit. Many existing verification methods suffer from unpredictability in their performance when they are applied. It is not clear whether they have to be run for seconds, hours, or days to return the verification results or whether they fail in the end. The unpredictability can only be resolved by ensuring complexity bounds. To guarantee scalability we are in particular interested in Polynomial Formal Verification (PFV), where the space and time complexities have polynomial bounds with respect to the size of the circuit.
The information about the design hierarchy is usually vital for PFV. The complex digital circuits consist of several components that cannot be verified with an individual verification technique in polynomial space and time. However, with additional knowledge about the boundaries of components, PFV becomes possible through the step-wise verification of sub-components and the use of different formal proof engines.
In this talk, we first introduce PFV and clarify its importance. We consider the verification of several flattened gate-level arithmetic circuits and illustrate the challenges of PFV when no design hierarchy is available. Then, we show how these challenges can be overcome by preserving design hierarchy information including the boundaries of the components.