The language xMAS has been designed by Intel with the purpose of modelling and verification of hardware.Recently, the language was extended with finite state machines to make it more expressive [19].Furthermore, it was shown how to prove liveness of such extended xMAS networks [19].Unfortunately, we demonstrate that the proof technique is unsound.We provide an alternative approach which we have carefully proven to be correct.Moreover, we show that our approach scales very well, which makes it possible to prove liveness properties at the system level.In particular, we show that using our approach, it is possible to verify a power control architecture composed of 1299 state machines representing 50 power domains where each domain contains 5 master and 5 slave devices.Proving liveness of this system takes less than 10 minutes.

In the realm of Multi-Processors System-on-Chip (MPSoC's), the Network-on-Chip (NoC) connecting all system components plays a crucial role in the overall correctness and performance of the system. Recent papers have proposed several ring based NoC solutions. The description and analysis of these micro-architectures are informal in nature. Text is used to argue about, e.g., deadlock freedom. For the first time, this paper proposes an environment for the formal modelling and analysis of such ring architectures with an emphasis on liveness properties. Our contribution includes a language to model ring micro-architectures, invariant generation techniques, deadlock freedom verification, and the application of our approach on a realistic case-study. The analysis reveals a possible deadlock not mentioned in the original paper.

To manage design complexity, high-level models are used to evaluate the functionality and performance of design solutions. There is a significant gap between these high-level models and the Register Transfer Level (RTL) implementations actually produced by designers. We address the challenge of bridging this gap, namely, relating abstract specifications to RTL implementations. An important feature of our proposed approach is to support non-deterministic specifications. From such a non-deterministic model, we automatically compute a representation of its observable behaviour. We then turn this representation into a System Verilog checker. The checker is connected to the input and output interfaces of the RTL implementation. The resulting combination is given to a commercial EDA tool to prove inclusion of the traces of the implementation into the traces of the specification. Our method is implemented for the formal micro-architectural description language (MaDL) - an extension of the xMAS formalism originally proposed by Intel - and exemplified on several examples.

We propose an algorithm for reachability analysis in micro-architectural models of communication fabrics. The main idea of our solution is to group transfers in what we call transfer islands. In an island, all transfers fire at the same time. To justify our abstraction, we give semantics of the initial models using a process algebra. We then prove that a transfer occurs in the transfer islands model if and only if the same transfer occurs in the process algebra semantics. We encode the abstract micro-architectural model together with a given state reachability property in the input format of nuXmv. Reachability is solved either using BDDs or IC3. Combined with inductive invariant generation techniques, our approach shows promising results.

In the realm of multi-core processors and systems-on-chip, communication fabrics constitute a key element. A large number of queues and distributed control are two important aspects of this class of designs. These aspects make decomposition and abstraction techniques difficult to apply. For this class of designs, the application of formal methods is a real challenge. In particular, the verification of liveness properties is often intractable. Communication fabrics can be seen as a set of queues and flops interconnected by combinatorial logic. Based on this simple but powerful observation, we propose a novel method for liveness verification. Our method directly applies to Register Transfer Level designs. The essential aspects of our approach are (1) to abstract away from the details of queue implementations and (2) an efficient encoding of liveness properties in an SMT instance. Experimental results are promising. Designs with hundreds of queues can be analysed for liveness within minutes.

In the multi-core era, on-chip communication networks are key to system correctness and performance. To deal with their growing complexity, micro-architectural models capture the intent of architects and provide means for formal analysis. However, the analysis of such micro-architectural models is restricted to non-scalable and/or very specific approaches. We present a novel scalable approach to support the symbolic channel type inference of large micro-architectural models described in the xMAS language proposed by Intel. We define an algorithm that computes all possible messages that can occur in a communication channel, treating their payload symbolically. These results can be used for further analysis such as verifying absence of misrouting, deriving inductive invariants and deadlock detection. We illustrate our approach on a Spidergon network developed at STMicroelectronics.

Deadlock freedom is a key challenge in the design of communication networks. Wormhole switching is a popular switching technique, which is also prone to deadlocks. Deadlock analysis of routing functions is a manual and complex task. We propose an algorithm that automatically proves routing functions deadlock-free or outputs a minimal counter-example explaining the source of the deadlock. Our algorithm is the first to automatically check a necessary and sufficient condition for deadlock-free routing. We illustrate its efficiency in a complex adaptive routing function for torus topologies. Results are encouraging. Deciding deadlock freedom is co-NP-Complete for wormhole networks. Nevertheless, our tool proves a 13 × 13 torus deadlock-free within seconds. Finding minimal deadlocks is more difficult. Our tool needs four minutes to find a minimal deadlock in a 11 × 11 torus while it needs nine hours for a 12 × 12 network.

This article presents a formal specification and validation environment to prove safety and liveness properties of parametric -- unbounded -- NoCs architectures described at a high-level of abstraction. The environment improves the GeNoC approach with two new theorems, proving evacuation and starvation freedom. The application of the validation methodology is illustrated on a HERMES NoC with adaptive west-first routing and wormhole switching. This case study illustrates the strong compositional aspect of the GeNoC environment. The complete specification of this HERMES instance, together with the proof that the specification is deadlock-free, starvation free, and all messages eventually leave the network at their correct destination, could be achieved in about a week. Approximately 86% of this proof is automatically derived from the GeNoC model.

Cache coherency is one of the major issues in multicore systems. Formal methods, in particular model-checking, have been successful at verifying high-level protocols, but, to the best of our knowledge, the verification of cache coherency at the architectural level is still an open issue. All existing verification efforts assume a reliable interconnect, that is, messages eventually reach their destination. We discuss the challenge of discharging this assumption at the architectural level where implementation details of the interconnect are mixed with a cache coherency protocol. Our automatic approach is based on a well-defined set of primitives to express architectural models, a generic model of communication fabrics expressed in an automated theorem proving system, and a dedicated algorithm for deadlock and livelock detection. We argue that reliability depends on the interaction between the interconnect and the cache coherency protocol. They must be verified altogether as their combination creates intricate message dependencies. We sketch our verification approach and apply it to a simple write-invalidate protocol on the Spidergon network-on-chip from STMicroelectronics. Our approach is promising. For this simple protocol, networks with tens of agents and hundreds of components can be analyzed within seconds.

Wormhole switching is a switching technique nowadays commonly used in networks-on-chips (NoCs). It is efficient but prone to deadlock. The design of a deadlock-free adaptive routing function constitutes an important challenge. We present a novel algorithm for the automatic verification that a routing function is deadlock-free in wormhole networks. A sufficient condition for deadlock-free routing and an associated algorithm are defined. The algorithm is proven complete for the condition. The condition, the algorithm, and the correctness theorem have been formalized and checked in the logic of the ACL2 interactive theorem proving system. The algorithm has a time complexity in O(N3), where N denotes the number of nodes in the network. This outperforms the previous solution of Taktak et al. by one degree. Experimental results confirm the high efficiency of our algorithm. This paper presents a formally proven correct algorithm that detects deadlocks in a 2D-mesh with about 4000 nodes and 15000 channels within seconds.

Deadlocks are an important issue in the design of interconnection networks. A successful approach is to restrict the routing function such that it satisfies a necessary and sufficient condition for deadlock-free routing. Typically, such a condition states that some (extended) dependency graph must be a cyclic. Defining and proving such a condition is complex. Proving that a routing function satisfies a condition can be complex as well. In this paper we present the first algorithm that automatically proves routing functions deadlock-free for store-and-forward networks. The time complexity of our algorithm is linear in the size of the resource dependency graph. The algorithm checks a variation of Duato's condition for adaptive routing. The condition and the algorithm have been formalized in the logic of the ACL2 interactive theorem prover. The correctness of our algorithm w.r.t. the condition is formally checked using ACL2.

The purpose of this comment is to show that Duato's condition for deadlock freedom is only sufficient and not necessary. We propose a fix to keep the condition necessary. The issue is subtle but essential: in a wormhole network worms necessarily do not intersect.

Wormhole switching is a popular switching technique in interconnection networks. This technique is also prone to deadlocks. Adaptive routing algorithms provide alternative paths that can be used to escape congested areas and prevent some deadlocks to occur. If not designed carefully, these new paths may as well introduce deadlocks. A successful solution to deadlock prevention is to constrain the routing function such that it does not introduce any deadlock. Many necessary and sufficient conditions for deadlock-free routing have been proposed. The definition and the proof of these conditions are complex and error-prone. These conditions are often counterintuitive and difficult to understand. Moreover, they are not static, as they all require the analysis of configurations, i.e., the network state. The contribution of this paper is twofold. We present the first static necessary and sufficient condition for deadlock-free routing in wormhole networks. Our condition is much simpler and requires less assumptions than all previous ones. It is formally proven correct using an automated proof assistant. In particular, our condition applies to incoherent routing functions which was considered an open problem. Second, we prove the deadlock decision problem co-NP-complete for wormhole networks.

Networks-on-chips (NoC) are emerging as a promising interconnect solution for efficient Multi-Processors Systems-on-Chips. We propose a methodology that supports the specification of parametric NoCs. We provide sufficient constraints that ensure deadlock-free routing, functional correctness, and liveness of the design. To illustrate our method, we discharge these constraints for a parametric NoC inspired by the HERMES architecture.

Multi-Processor Systems-on-Chip (MPSoC) designs are constructed by assembling pre-designed parameterized components. Communications are crucial to their overall functionality and performance. Formal verification methods have been intensively applied to processing elements, e.g., microprocessors. Very little work has been done with respect to communication modules. We present the formal specification of a packet switched NoC and its proven refinement. At the specification level, routing decisions are computed at once before packets get injected in the network. In the implementation, routing decisions are distributed over each individual node. We prove that the implementation behaves according to its specification for a 2D-mesh NoC. All models and proofs have been checked using the ACL2 theorem proving system. To the best of our knowledge, this work constitutes the first cross-layer verification of on-chip communication networks.

Abstract This paper presents a formal model and a systematic approach to the validation of communication architectures at a high level of abstraction. This model is described mathematically by a function, named GeNoC . The correctness of GeNoC is expressed as a theorem, which states that messages emitted on the architecture reach their expected destination without any modification of their content. The model identifies the key constituents common to all on chip communication architectures, and their essential properties from which the correctness theorem is deduced. Each constituent is represented by a function that has no explicit definition but is constrained to satisfy the essential properties. Thus, the validation of a particular architecture is reduced to the proof that its concrete definition satisfies the essential properties. In practice, the model has been defined in the logic of the ACL2 theorem proving system. We illustrate our approach on several architectures that constitute concrete instances of the generic GeNoC model. Some of these applications come from industrial designs, such as the AMBA AHB bus or the Octagon network from ST Microelectronics.

We develop formal arguments about a bit clock synchronization mechanism for time-triggered hardware. The architecture is inspired by the FlexRay standard and described at the gate-level. The synchronization algorithm relies on a specific value of a counter. We prove or disprove values proposed in the literature. Our framework is based on a general and precise model of clock domain crossing, which considers metastability and clock imperfections. Our approach combines this model with the state transition representation of hardware. The result is a clear separation of analog and digital behaviors. Analog considerations are formalized in the logic of the Isabelle/HOL theorem prover. Digital arguments are discharged using the NuSMV model checker. To the best of our knowledge, this is the first verification effort tackling asynchronous transmissions at the gate-level.

Networks on chip are emerging as a promising solution for the design of complex systems on a chip, to interconnect manufactured IP cores, and the need to formally guarantee their correctness is crucial. In a NoC centered design, the individual IP's are considered already validated. This paper addresses the validation of the communication infrastructure. A generic formal model for NoC's has been developed and implemented in the ACL2 theorem prover. As an application, the HERMES network has been formalized in this model, and we show that both formal proofs and simulation experiments can be performed in ACL2

We present a formal model of the bit transmission between registers with arbitrary clock periods. Our model considers precise timing parameters, as well as metastability. We formally define the behavior of registers over time. From that definition, we prove, under certain conditions, that data are properly transmitted. We discuss how to incorporate the model in a purely digital model. The hypotheses of our main theorem define conditions that must be satisfied by the purely digital part of the system to preserve correctness