System Level Verification of Phase-Locked Loop using Metamorphic Relations
Shubham Rai6,a, Walter Lau Neto11,b, Yukio Miyasaka11,12, Xinpei Zhang1, Mingfei Yu1, Qingyang Yi1, Masahiro Fujita1, Guilherme B. Manske2, Matheus F. Pontes2, Leomar S. da Rosa Junior2, Marilton S. de Aguiar2, Paulo F. Butzen2, Po-Chun Chien3, Yu-Shan Huang3, Hoa-Ren Wang3, Jie-Hong R. Jiang3, Jiaqi Gu4, Zheng Zhao4, Zixuan Jiang4, David Z. Pan4, Brunno A. de Abreu5,9, Isac de Souza Campos5,9, Augusto Berndt5,9, Cristina Meinhardt5,9, Jonata T. Carvalho5,9, Mateus Grellert5,9, Sergio Bampi5, Aditya Lohana6, Akash Kumar6, Wei Zeng7, Azadeh Davoodi7, Rasit O. Topaloglu7, Yuan Zhou8, Jordan Dotzel8, Yichi Zhang8, Hanyu Wang8, Zhiru Zhang8, Valerio Tenace10, Pierre-Emmanuel Gaillardon10, Alan Mishchenko11,c, and Satrajit Chatterjee12,d
1University of Tokyo, Japan
2Universidade Federal de Pelotas, Brazil
3National Taiwan University, Taiwan
4University of Texas at Austin, USA
5Universidade Federal do Rio Grande do Sul, Brazil
6Technische Universitaet Dresden, Germany
7University of Wisconsin–Madison, USA
8IBM, USA
9Cornell University, USA
10Universidade Federal de Santa Catarina, Brazil
11University of Utah, USA
12UC Berkeley, USA, pGoogle AI, USA
ashubham.rai@tu-dresden.de
bwalter.launeto@utah.edu
calanmi@berkeley.edu
dschatter@google.com
ABSTRACT
Logic synthesis is a fundamental step in hardware design whose goal is to find structural representations of Boolean functions while minimizing delay and area. If the function is completely-specified, the implementation accurately represents the function. If the function is incompletely-specified, the implementation has to be true only on the care set. While most of the algorithms in logic synthesis rely on SAT and Boolean methods to exactly implement the care set, we investigate learning in logic synthesis, attempting to trade exactness for generalization. This work is directly related to machine learning where the care set is the training set and the implementation is expected to generalize on a validation set. We present learning incompletely-specified functions based on the results of a competition conducted at IWLS 2020. The goal of the competition was to implement 100 functions given by a set of care minterms for training, while testing the implementation using a set of validation minterms sampled from the same function. We make this benchmark suite available and offer a detailed comparative analysis of the different approaches to learning.
