CFP last date
20 January 2025
Reseach Article

Equivalence Checking using Assertion based Technique

by Shailesh Kumar, Sameer Arvikar, Saurabh Jha, Tarun K. Gupta
International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 120 - Number 14
Year of Publication: 2015
Authors: Shailesh Kumar, Sameer Arvikar, Saurabh Jha, Tarun K. Gupta
10.5120/21299-4349

Shailesh Kumar, Sameer Arvikar, Saurabh Jha, Tarun K. Gupta . Equivalence Checking using Assertion based Technique. International Journal of Computer Applications. 120, 14 ( June 2015), 39-43. DOI=10.5120/21299-4349

@article{ 10.5120/21299-4349,
author = { Shailesh Kumar, Sameer Arvikar, Saurabh Jha, Tarun K. Gupta },
title = { Equivalence Checking using Assertion based Technique },
journal = { International Journal of Computer Applications },
issue_date = { June 2015 },
volume = { 120 },
number = { 14 },
month = { June },
year = { 2015 },
issn = { 0975-8887 },
pages = { 39-43 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume120/number14/21299-4349/ },
doi = { 10.5120/21299-4349 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T23:06:15.447197+05:30
%A Shailesh Kumar
%A Sameer Arvikar
%A Saurabh Jha
%A Tarun K. Gupta
%T Equivalence Checking using Assertion based Technique
%J International Journal of Computer Applications
%@ 0975-8887
%V 120
%N 14
%P 39-43
%D 2015
%I Foundation of Computer Science (FCS), NY, USA
Abstract

This paper presents approach to equivalence checking methodology for large analog/mixed signal systems such as HDMI-PHY, USB-PHY (Transceiver). We verify the equivalence between a behavioral model and its electrical equivalent (Spice netlist) by applying same inputs to both representations. Inputs to spice are given through a D2A. The output waveforms are then compared to find the equivalence. We have implemented SystemVerilog assertions for critical timing checks. We are using digital-on-top (DoT) approach, SystemVerilog assertions are applied in the testbench, means the same assertions are applied to behavioral output as well as to the output of spice which is converted from analog to digital. We have given margin (rise/fall time) in assertions to ensure that assertion should comply with the allowed difference in spice and model output. The proposed methodology is then applied for equivalence checking of USB-PHY transceiver as a test case.

References
  1. M. H. Zaki et al, "Formal verification of analog and mixed signal designs: a survey", Microelectronics Journal, 39(2008), pp. 1395-1404.
  2. Amandeep Singh and Peng Li, "On behavioral model equivalence checking for large analog/mixed signal systems", Proceedings of the IEEE International Conference on Computer-Aided Design, San Jose, California (2010).
  3. H. Parekh et al, "Equivalence Validation of Analog Behavioral Models", DVCon United States (2014).
  4. Universal Serial Bus 2. 0 Specification, USB Implementers Forum, (2000).
  5. R. Mekkadan, "Functional Verification of CSI-2 Rx-PHY using AMS Co-simulations", DVCon India (2014).
  6. Questa ADMS Reference Manual, Mentor Graphics.
  7. EZWave Reference Manual, Mentor Graphics
  8. C. Ming song and P. Mishra, 'Assertion-Based Functional Consistency Checking between TLM and RTL Models', in 26th International Conference on VLSI Design and the 12th International Conference on Embedded Systems, 2013, pp. 320-325
Index Terms

Computer Science
Information Sciences

Keywords

Transceiver Equivalence Assertion.