S.P. Khatri and A. Narayan and S.C. Krishnan and K.L. McMillan and Alberto L. Sangiovanni-Vincentelli and Robert K. Brayton

EECS Department, University of California, Berkeley

Technical Report No. UCB/ERL M95/50

, 1995

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1995/ERL-95-50.pdf

In this paper, we address the problem of Engineering Change in a non-deterministic finite state machine framework. We are given a deterministic implementation FSM, and a non-deterministic specification FSM, such that the implementation does not meet the specification. The problem consists of controlling the implementation FSM in such a way that for all possible sequences of external inputs, the generated outputs are allowed in the specification. We propose a new formalism for the Engineering Change problem which is applicable to non-deterministic specifications. We use the notion of Simulation Relations from the theory of concurrent systems, to develop this new formalism. Our method is cast in the form of a simulation of the implementation by the specification. We prove the necessary and sufficient condition for the existence of a solution to the problem. We also provide an algorithm to obtain all possible solutions under this setting. We have implemented this algorithm, using implicit state enumeration and Reduced Ordered Binary Decision Diagrams (ROBDDs). An important feature of our method is that the algorithm gives us a solution which is correct by construction, and accordingly we do not need to perform a separate verification step in the design.

---

BibTeX citation:

@techreport{Khatri:M95/50,
    Author= {Khatri, S.P. and Narayan, A. and Krishnan, S.C. and McMillan, K.L. and Sangiovanni-Vincentelli, Alberto L. and Brayton, Robert K.},
    Title= {An Engineering Change Methodology Using Simulation Relations},
    Year= {1995},
    Month= {Apr},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1995/2795.html},
    Number= {UCB/ERL M95/50},
    Abstract= {In this paper, we address the problem of Engineering Change in a non-deterministic finite state machine framework. We are given a deterministic implementation FSM, and a non-deterministic specification FSM, such that the implementation does not meet the specification. The problem consists of controlling the implementation FSM in such a way that for all possible sequences of external inputs, the generated outputs are allowed in the specification. We propose a new formalism for the Engineering Change problem which is applicable to non-deterministic specifications. We use the notion of Simulation Relations from the theory of concurrent systems, to develop this new formalism. Our method is cast in the form of a simulation of the implementation by the specification. We prove the necessary and sufficient condition for the existence of a solution to the problem. We also provide an algorithm to obtain all possible solutions under this setting. We have implemented this algorithm, using implicit state enumeration and Reduced Ordered Binary Decision Diagrams (ROBDDs). An important feature of our method is that the algorithm gives us a solution which is correct by construction, and accordingly we do not need to perform a separate verification step in the design.},
}

EndNote citation:

%0 Report
%A Khatri, S.P. 
%A Narayan, A. 
%A Krishnan, S.C. 
%A McMillan, K.L. 
%A Sangiovanni-Vincentelli, Alberto L. 
%A Brayton, Robert K. 
%T An Engineering Change Methodology Using Simulation Relations
%I EECS Department, University of California, Berkeley
%D 1995
%@ UCB/ERL M95/50
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1995/2795.html
%F Khatri:M95/50