International Research Journal of Engineering and Technology (IRJET)
e-ISSN: 2395-0056
Volume: 09 Issue: 09 | Sep 2022
p-ISSN: 2395-0072
www.irjet.net
Formal Verification Of An Intellectual Property In a Field Programmable Gate Array Prashanth M1, Sujatha K2 1Department
of Electronics and communication, BMS college of engineering, Bangalore, India Professor, Dept. of Electronics and communication, BMS college of engineering, Bangalore, India ---------------------------------------------------------------------***--------------------------------------------------------------------2 Associate
Abstract - The verification method has fallen behind,
design specifications. The main types of equivalence checking in formal verification is logical equivalence checking and sequential equivalence checking. Logical equivalence checking, sometimes referred to a process known as combinational equivalence checking, procedure of determining if two architectures share the same combinational logic between registers. The number of registers in the two designs under comparison need to be equal as well. This method is used to confirm that two designs with various levels of abstraction, like a gate-level netlist, are functionally similar and a layout netlist are functionally equivalent[3].
nevertheless, as a result of increased IC production capabilities. The verification phase of the circuit design flow, according to ITRS, has taken the longest. Verification engineers now outnumber design engineers in terms of the number of active engineering projects. Verification is now the IC design industry's bottleneck since the ratio for sophisticated designs might approach 2:1 or 3:1. Verification will become the main obstacle for the future growth of the IC design business if significant advancements are not made. Our suggested formal verification will compare the reference model with the implementation model using Jasper Gold formal verification tool. With the necessary design changes made without sacrificing functionality, we were able to achieve an assertion pass rate of 80%.
The technique of confirming that whether two designs specifications are equivalent or not and produce the similar results when given the similar inputs is known as sequential equivalence checking. The sequential logic of two designs, which may have different implementations, is compared by the SEC as shown in figure 1.1.
Key Words: Formal verification, Intellectual property,
counter example, Sequential equivalence checking, Combinational equivalence checking.
Some more logic, including scan-based logic, power control circuits, etc. Verification of such modifications is required. Regular verification processes take a long period, which extends the time to market. The changed design is compared to the golden design using sequential equivalence testing to ensure that they are functionally equal.
1. INTRODUCTION Formal verification is the process of utilizing mathematical tools to confirm the accuracy of the design. Timing checks are not carried out by formal verification tools, which instead utilize a variety of techniques to verify the design. Since these tools don't require a test bench or stimulus, once an RTL code is ready, formal verification can be carried out, A bug is easier to correct the sooner it is discovered[1]. Formal verification techniques find bugs that are missed by standard verification methods. Moreover, formal verification typically identifies flaws rather more quickly than standard methods do in cases when they are detectable. A design first should undergo formal verification before being functionally tested through simulation and emulation. Essentially, the DUT is a network of flip-flops and logical gates. Equations may be used to express this network of gates and flip-flops. The tool then independently evaluates each checker (i.e., SVA assertion), looking for any possible input sequences that might show the checker to be untrue. If such a sequence is discovered, a waveform illustrating this erroneous situation is shown. This waveform is known as a counter example in formal language (CEX)[5].
Fig -1: Sequential Equivalence Checking The ideal candidates for formal verification are these short, control-oriented pieces that are repeated frequently. All of Written assertions and assumptions for the design and interaction using SVA. In order to ensure that every component is covered during formal verification of the
The goal of formal verification is to detect the bugs in the early stage of the design and in less time, we can verify the
© 2022, IRJET
|
Impact Factor value: 7.529
|
ISO 9001:2008 Certified Journal
|
Page 1055