Formal design and verification of on chip networking

In this paper the formal design of networks and verification of on chip networking is presented in this paper. Basic octagon architecture with bidirectional links is demonstrated for this analysis. An octagon packet is the data that must be carried from the source node to the destination node. A network on chip model, written in a standard design language (VHDL) and the behavior is simulated on traffic hypotheses. An assertion-based verification in TheoSim is used to prove the expression satisfies the properties. The method is supported by a combination of simulation and symbolic reasoning engines that bridges the gap between specification and implementation debugging.