International Research Journal of Engineering and Technology (IRJET)
e-ISSN: 2395-0056
Volume: 04 Issue: 07 | July -2017
p-ISSN: 2395-0072
www.irjet.net
A General Framework for Electronic Circuit Verification Afsal K Assistant Professor, Dept. of Computer Science, Malabar College of Advanced Studies, Kerala, India
----------------------------------------------------------------------------***----------------------------------------------------------------------------Abstract - The design and implementation of digital software system can be considered as a mathematical electronic circuits is to undergo proper testing so that bugs model, verification of certain properties would be really can be eliminated from the development environment itself. easy. That is the whole idea behind program verification. Since digital electronic circuits and computer programs are similar in nature, methods adopted in program verification A program may have a large number of components like can be effectively used for the verification of digital systems variables, semaphores, locking mechanisms etc. and it is also. Formal modelling is an important method in any kind really hard to determine and verify all the features of all of verification and in this paper, we present a novel the components. Hence we limit the components and approach to formally modeling a digital system. We prove features. As an example, consider the following program that our approach can be used for modeling digital systems segment. with any number of gates as the resulting model will have a finite number of states only. We use LTL to specify for (;;) { properties of digital systems and we use a symbolic model checker to verify those properties. x = 0; ..... Key Words: Digital electronic systems, program x = 1; verification for digital systems, LTL for specifying } properties of digital systems, formal modelling, using SAL for verification Here we would like to verify the properties of x only. Hence we convert the program as a finite state machine 1. INTRODUCTION with two states, i.e., x=0 and x=1, as shown in figure1. Proving correctness of programs have always been a hot topic in the realm of computer science. The software systems always stressed the importance of testing from the very beginning and as a result, software development life cycle (SDLC) always had an important component in testing [1]. A software does not turn out to be usable unless it passes the test cases prepared by the testing team. Modern day SDLC systems present large number of testing methods to avoid any minor defect in the software. Although the present black box testing is sufficient for a large number of software applications as a passing criterion, there are certain mission critical applications where the present black box testing is not enough. On June 4, 1996, the unmanned rocket Ariane 5 (from European Space Agency) exploded just after 40 seconds from its launch. On detailed evaluation later, it was found out that a 64-bit integer relating to its velocity component was converted to a 16-bit integer [2]. The system had passed all the black box test cases, though it is not easy for that kind of testing to reveal the bug.
Figure 1. Transition system for the states of the variable x. The start and final states of the automaton are not shown in figure 1 as the variable x does not feature them. Hence it is rather a transition system than a deterministic finite automaton. However, the transition system itself is powerful enough to prove certain properties of the program. For example, suppose we want to verify that the value of x is always either 0 or 1. It is very easy for a model checker to do the above, given the above verification condition is
We need a better system which can figure out the bugs and thereby verifying the correctness of the program. Since it is not even possible to run and verify certain systems, it would be really beneficial if there is a testing / verification. system which predicts errors by static analysis of the code / algorithm. Moreover, if the entire
Š 2017, IRJET
|
Impact Factor value: 5.181
|
ISO 9001:2008 Certified Journal
|
Page 1469