Learning framework for software-hardware model generation and verification

Abstract

Generating an abstract model of the behavior of a hardware and/or software design. A learning framework learns an unknown regular language that represents the behaviors of the hardware and/or software logic which do not violate a specified property that the abstract model is required to satisfy. The framework receives input data including the specified property, concrete models of the behavior of the hardware and/or software; and an alphabet of all symbols that are allowed to occur in any string that can be defined in the unknown regular language, each symbol representing an event in the hardware and/or software. The framework generates an abstract model of the behavior of the hardware or software design by checking whether a sequence of events in a concrete model satisfies the specified property and outputs the generated abstract model.

What is claimed is: 
     
       1. A computer-implemented method comprising:
 receiving input data including: a required occurrence that an abstract model is required to produce, a concrete software model representing a software behavior, the software behavior corresponding to execution of software logic, and a set of all symbols allowed to occur in any string that can be defined in a specified regular language, each symbol representing an individual event occurring during execution of the software logic, each string describing a sequence of events representing the software behavior; 
 checking whether a first event in a first sequence of events produced by the concrete software model satisfies the required occurrence; 
 learning the specified regular language representing the software behavior according to the concrete software model that produces the first event, the learned regular language being represented by strings; 
 learning a function call hierarchy of the software behavior, wherein the function call hierarchy is the sequence of functions executed by the program; 
 modifying code of the concrete software model by adding at least one additional variable that generates an observable event in response to one or more conditions being met, and the function call hierarchy that generated the observable event, wherein the concrete software model is configured such that at least one hidden event is generated when one or more conditions are met, the hidden event not being observable by any program routine outside of the concrete software model, and further wherein the observable event being observable by a program routine outside of the concrete software model; 
 generating an abstract software model of the software behavior, the generated abstract software model satisfying the required occurrence, wherein the abstract software model is generated using assume-guarantee reasoning; and 
 outputting the generated abstract software model. 
 
     
     
       2. The computer-implemented method of  claim 1 , further comprising:
 co-verifying a software-hardware co-design group by checking whether a second event in a second sequence of events produced by a concrete hardware model representing a hardware behavior, the hardware behavior corresponding to execution of hardware logic, satisfying the required occurrence; 
 generating an abstract hardware model of the hardware behavior, the generated abstract hardware model satisfying the required occurrence; and 
 outputting a set of co-verified abstract models including the generated abstract software model and the generated abstract hardware model; 
 wherein: 
 the required occurrence is a plurality of events including the first event and the second event; 
 the software logic is associated with the hardware logic as a member of the software-hardware co-design group; 
 the input data further includes the concrete hardware model of the hardware behavior; 
 the set of all symbols further includes symbols representing individual events occurring in the hardware logic; and 
 the learned regular language further represents the hardware behavior. 
 
     
     
       3. The computer-implemented method of  claim 2 , further comprising:
 responsive to the outputting step, automatically translating the set of co-verified abstract models into an executable software program and a specification of a hardware module, the specification being coded in a hardware description language. 
 
     
     
       4. The computer-implemented method of  claim 2 , further comprising:
 receiving an original concrete hardware model of the hardware logic specified in a hardware description language; and 
 transforming the original concrete hardware model into the concrete hardware model being executable program code specified in a software program language. 
 
     
     
       5. The computer-implemented method of  claim 2 , wherein the input data further includes a specified count indicating a maximum number of symbols that are concatenated for generating a string representing a sequence of events simulated in the concrete software model. 
     
     
       6. The computer-implemented method of  claim 5 , wherein:
 the hardware logic is a clock; and 
 the specified count is the number of clock cycles of the clock to be considered when checking whether a simulation of the sequence of events in the concrete hardware model satisfies the required occurrence. 
 
     
     
       7. The computer-implemented method of  claim 6 , wherein checking whether a simulation of the sequence of events in the concrete hardware model satisfies the required occurrence includes:
 executing a hardware model checker such that the sequence of events occurs in the hardware model checker, and 
 reporting the sequence of events for comparing to each string representing the hardware behavior. 
 
     
     
       8. The computer-implemented method of  claim 1 , where the abstract software model is generated as a deterministic finite automaton (DFA). 
     
     
       9. The computer-implemented method of  claim 1 , the abstract software model being generated as a collection of quantified Boolean formulas. 
     
     
       10. The computer-implemented method of  claim 1 , the set of all symbols being selected from the group consisting of:
 a module alphabet consisting of symbols respectively representing a module of the software logic, the instantiation of the modules being the events represented by the symbols, each string of the module alphabet describing a sequence of instantiating modules; 
 a function alphabet consisting of symbols respectively representing a function of the software logic, the calling of the functions being the events represented by the symbols, each string of the function alphabet describing a sequence of functions calling each other; 
 a control alphabet consisting of symbols respectively representing a control statement being implemented by the software logic, the execution of the control statements being the events represented by the symbols, each string of the control alphabet describing a sequence of control statements sequentially executed in a series of causally-connected events; 
 a data alphabet consisting of symbols respectively representing an event being thrown by the software logic upon assigning a particular value to a particular parameter that is monitored and/or controlled by the software logic; and 
 a user-defined alphabet comprising symbols of one or more of the module alphabet, the function alphabet, the control alphabet, and the data alphabet. 
 
     
     
       11. The computer-implemented method of  claim 1 , wherein the method is implemented in a model generation framework including:
 a first teacher module that obtains knowledge of the specified regular language by simulating one or more events in the concrete software model; 
 a second teacher module that obtains knowledge of the learned regular language by simulating a candidate abstract model in the form of an automaton, the simulation comprising analyzing one or more strings representing sequences of events in the concrete software model; and 
 a learner module that learns the specified regular language by sending membership queries to the first teacher module and by sending conjecture queries based on the learned regular language to the second teacher module. 
 
     
     
       12. The computer-implemented method of  claim 11 , wherein generating the abstract software model includes:
 generating, by the learner module, a plurality of strings by concatenating symbols of the set of all symbols; 
 sending, by the learner module, a membership query for each string to the first teacher module; 
 checking, by the first teacher module, whether each string belongs to the specified regular language including:
 executing the concrete software model such that a corresponding sequence of events described by each string is simulated as occurring in the concrete software model, the concrete software model generating signals, and 
 checking whether the generated signals satisfy the required occurrence; and 
 
 returning, by the first teacher module, a confirming result of the checking steps for each string to the learner module, the confirming result being: (i) that the string belongs to the specified regular language where the signals satisfy the required occurrence, or (ii) that the string does not belong to the specified regular language where the signals do not satisfy the required occurrence. 
 
     
     
       13. The computer-implemented method of  claim 12 , wherein generating the abstract software model further includes:
 receiving, by the learner module, the result of the checking steps for each string; 
 responsive to the result, generating, by the learner module, a first abstract software model representing the software behavior for transitioning from one state to a next state when processing events; 
 sending, by the learner module, the first abstract software model in the conjecture query based on the learned regular language to the second teacher module; 
 determining, by the second teacher module, whether a formal language represented by the first abstract software model is equal to the learned regular language of the concrete software model, the determination including:
 executing the first abstract software model to simulate the software behavior, 
 determining whether signals generated during this simulation satisfy the required occurrence; and 
 
 returning, by the second teacher module, a simulation result of the determining steps, the simulation result being: (i) that the first abstract software model does not satisfy the required occurrence, or (ii) that the first abstract software model does satisfy the required occurrence. 
 
     
     
       14. The computer-implemented method of  claim 13 , further comprising:
 responsive to receiving the simulation result that the first abstract software model does satisfy the required occurrence, outputting the first abstract software model as the generated abstract software model. 
 
     
     
       15. A computer program product comprising:
 one or more computer readable storage devices and program instructions stored on the one or more computer readable storage devices, the stored program instructions comprising: 
 program instructions to receive input data including: a required occurrence that an abstract model is required to produce, a concrete software model representing a software behavior, the software behavior corresponding to execution of software logic, and a set of all symbols allowed to occur in any string that can be defined in a specified regular language, each symbol representing an individual event occurring in the software logic, each string describing a sequence of events representing the software behavior; 
 program instructions to check whether a first event in a first sequence of events produced by the concrete software model satisfies the required occurrence; 
 program instructions to learn the specified regular language representing the software behavior according to the concrete software model that produces the first event, the learned regular language being represented by strings; 
 program instructions to learn a function call hierarchy of the software behavior, wherein the function call hierarchy is the sequence of functions executed by the program; 
 program instructions to modify code of the concrete software model by adding at least one additional variable that generates an observable event in response to one or more conditions being met, and the function call hierarchy that generated the observable event, wherein the concrete software model is configured such that at least one hidden event is generated when one or more conditions are met, the hidden event not being observable by any program routine outside of the concrete software model, and further wherein the observable event being observable by a program routine outside of the concrete software model; 
 program instructions to generate an abstract software model of the software behavior, the generated abstract software model satisfying the required occurrence, wherein the abstract software model is generated using assume-guarantee reasoning; and 
 program instructions to output the generated abstract software model. 
 
     
     
       16. The computer program product of  claim 15 , wherein the computer readable storage media has further stored thereon:
 program instructions to co-verify a software-hardware co-design group by checking whether a second event in a second sequence of events produced by a concrete hardware model representing a hardware behavior, the hardware behavior corresponding to execution of hardware logic, satisfying the required occurrence; 
 program instructions to generate an abstract hardware model of the hardware behavior, the generated abstract hardware model satisfying the required occurrence; and 
 program instructions to output a set of co-verified abstract models including the generated abstract software model and the generated abstract hardware model; 
 wherein: 
 the required occurrence is a plurality of events including the first event and the second event; 
 the software logic is associated with the hardware logic as a member of the software-hardware co-design group; 
 the input data further includes the concrete hardware model of the hardware behavior; 
 the set of all symbols further includes symbols representing individual events occurring in the hardware logic; and 
 the learned regular language further represents the hardware behavior. 
 
     
     
       17. A computer system comprising:
 one or more computer processors; 
 one or more computer readable storage media; and 
 program instructions stored on the one or more computer readable storage media for execution by at least one of the one or more computer processors, the stored program instructions comprising: 
 program instructions to receive input data including: a required occurrence that the abstract model is required to produce, a concrete software model representing a software behavior, the software behavior corresponding to execution of software logic, and a set of all symbols allowed to occur in any string that can be defined in a specified regular language, each symbol representing an individual event occurring in the software logic, each string describing a sequence of events representing the software behavior; 
 program instructions to check whether a first event in a first sequence of events produced by the concrete software model satisfies the required occurrence; 
 program instructions to learn the specified regular language representing the software behavior according to the concrete software model that produces the first event, the learned regular language being represented by strings; 
 program instructions to learn a function call hierarchy of the software behavior, wherein the function call hierarchy is the sequence of functions executed by the program; 
 program instructions to modify code of the concrete software model by adding at least one additional variable that generates an observable event in response to one or more conditions being met, and the function call hierarchy that generated the observable event, wherein the concrete software model is configured such that at least one hidden event is generated when one or more conditions are met, the hidden event not being observable by any program routine outside of the concrete software model, and further wherein the observable event being observable by a program routine outside of the concrete software model; 
 program instructions to generate an abstract software model of the software behavior, the generated abstract software model satisfying the required occurrence, wherein the abstract software model is generated using assume-guarantee reasoning; and 
 program instructions to output the generated abstract software model. 
 
     
     
       18. The computer system of  claim 17 , wherein the program instructions further include:
 program instructions to co-verify a software-hardware co-design group by checking whether a second event in a second sequence of events produced by a concrete hardware model representing a hardware behavior, the hardware behavior corresponding to execution of hardware logic, satisfying the required occurrence; 
 program instructions to generate an abstract hardware model of the hardware behavior, the generated abstract hardware model satisfying the required occurrence; and 
 program instructions to output a set of co-verified abstract models including the generated abstract software model and the generated abstract hardware model; 
 wherein: 
 the required occurrence is a plurality of events including the first event and the second event; 
 the software logic is associated with the hardware logic as a member of the software-hardware co-design group; 
 the input data further includes the concrete hardware model of the hardware behavior; 
 the set of all symbols further includes symbols representing individual events occurring in the hardware logic; and 
 the learned regular language further represents the hardware behavior.