The Abstraction Research And Application Based On GSTE

As society progresses, the impact of the integrated circuit in society is getting bigger, accounted for a rising proportion. From the cell phones, tablet personal computers in daily use throughout the supported country technology, such as, the satellite, space shuttle, integrated circuits have been in our lives. With the increasing development of technology, the complexity of integrated circuits is also increasing exponentially. How to ensure the reliability of integrated circuits work correctly has become the focus of current research. From traditional testing/simulation to the rising formal verification methods, all of these methods are combined correctly in order to ensure reliable operations. During the study of generalized symbolic trajectory evaluation in formal methods, it finds that the relation between integrated circuit Boolean modeling and biological gene regulation network modeling, and innovatively applies the formal methods to the modeling and calculation of biological gene regulatory network, besides having a lot of work to reduce the complexity of integrated circuits and improve computational efficiency.The main results of the work and innovations are as follows:1. Reducing the complexity of integrated circuits and improving computational efficiency, it innovatively proposes an algorithm of generalized symbolic trajectory evaluation: minimum preserved consequence abstraction algorithm, and corrects the false negative due to excessive abstraction, and proposes a new minimum preserved consequence abstraction algorithm. Finally the two proposed algorithms successfully applied to the verification tool developed independently: Whale verification platform. The experimental results show that the efficiency and correctness of the proposed algorithm.2. In the application of generalized symbolic trajectory evaluation, it innovatively applies algorithms to test the NAND Flash software simulator model. Combining the experimental results and results of formal methods, the approach to protect the NAND Flash software simulator design is correct.3. Establishing the biological aspects of gene regulatory networks in the model, it finds an association between biological gene regulatory networks with Boolean networks, which has a lot to think in Boolean modeling of integrated biological gene regulatory networks with Boolean modeling process similarities, and innovation will be a combination of both, the integrated circuit modeling method is applied to some biological gene regulatory network model creation process successfully.4. Computing synchronization attractor of gene regulatory networks, it innovatively synchronizes attractor into three categories, no branch attractor, attractor branch presence and full branch attractor, and proposes an algorithm to calculate synchronized attractors in synchronous Boolean network. However, due to redundant computing of the above algorithm, it propose an optimized algorithm to calculate synchronized attractors in synchronous Boolean network, and compare the difference of these proposed algorithms. Finally, comparing the two algorithms with existing computing Boolean network synchronization tool for synchronize attractors: BoolNet, three groups based on biological experiments are compared to corroborator algorithm efficiency.5. After further research, asynchronous Boolean networks would be more fitting to biological gene regulatory networks in biological signal transduction than synchronous Boolean networks. In biological gene regulatory networks asynchronous attractor computing, it innovatively merge the synchronous attractors with the asynchronous attractors and divide them into four categories, self-loop attractor, simple loop attractor, synchronous complex loop attractor and asynchronous complex loop attractor. According to the synchronous and asynchronous attractors’ internal characteristics, it analyzes synchronous and asynchronous attractors’ relation and proposes an algorithm for computing and classifying asynchronous Boolean networks’ attractors. In the experiment section, the above algorithm is implemented as GeneFatt kit. Compared with existing computing tool, GenYsis, experimental results show the superiority of GeneFatt toolkit.