Professor Emeritus
Professor in the Graduate School
Electrical Engineering and Computer Sciences Department
University of California, Berkeley, California, USA

 

Webpage

Synthesis for Verification

Thursday, 10 December 2015 at 14:00 in room BC 420

 

Abstract:

It is not surprising that synthesis plays a key role in formal verification where many problems are posed as a sequential circuit with one primary output (PO). The output can represent the miter of two circuits where one may be the original specification representing the “golden model” and the other an optimized version. A miter is the OR of the pair-wise XOR of corresponding PO pairs from the two circuits. If the circuits are equivalent, then the PO pairs must agree for all clock cycles resulting in the output of the miter being always 0. Similarly the single output can represent a property to be proved about the design, where the output is 0 if and only if the property holds forever.

In theory, if synthesis were powerful enough, it could re-synthesize the entire circuit down to the constant 0. Although this happens sometimes, most often the circuit is only reduced in terms of its number of flip-flops and size of its logic. This does not answer the verification problem, but does help down-stream verification engines, which often work better on smaller circuits.

Berkeley’s ABC system involves both synthesis and verification, which share many fundamental data-structures and basic algorithms. Its main verification system, super_prove, has a sophisticated initial simplification phase, which is one of the reasons that it has won the hardware model-checking competition for the last four years. The simplification part employs a series of “synthesis” transformations which preserve the I/O behavior and were originally developed for synthesis. These include

•    retiming (minimum area and most forward),
•    signal correspondence,
•    phase abstraction,
•    temporal decomposition,
•    rewriting,
•    sequential cleanup,
•    constraint extraction, and
•    reparametrization.

In this talk we will give a brief overview of each of these “synthesis” transformations.

About the speaker:

Robert Brayton received the BSEE degree from Iowa State University in 1956 and the Ph.D. degree in mathematics from MIT in 1961. He was a member of the Mathematical Sciences Department of the IBM T. J. Watson Research Center until he joined the EECS Department at Berkeley in 1987. He held the Edgar L. and Harold H. Buttner Endowed Chair and the Cadence Distinguished Professor of Electrical Engineering at Berkeley. Currently he is a Professor in the Graduate School at Berkeley. He is a member of the US National Academy of Engineering, and a Fellow of the IEEE. Awards include

-    1971 IEEE Guilleman-Cauer best paper award,
-    1987 ISCAS Darlington best paper award,
-    1991 IEEE CAS Technical Achievement award
-    2002 Iowa State University Marston Engineering Medal,
-    2006, IEEE Emanuel R. Piore award
-    2006 ACM Kanallakis award
-    2006 EDAA lifetime achievement award
-    2007 EDAC/CEDA Phil Kaufman award
-    2008 D. O. Pederson Best Paper in IEEE Trans. on CAD award
-    2009 ACM/IEEE Richard Newton Technical Impact award
-    2010 Iowa State University Outstanding Alumnus award
-    2011 The SRC Technical Excellence award
-    2011 ACM/SIGDA Pioneering Achievement award

He has authored over 450 technical papers, and 11 books in the areas of the analysis of nonlinear networks, simulation and optimization of electrical circuits, logic synthesis, and formal design verification.