With increasing clock frequencies, the signal delay on some interconnects in a System on Chip (SoC) often exceeds the clock period, which necessitates latency insensitive protocols (LIPs). The correctness of a system composed of synchronous blocks communicating via LIPs is established by showing latency equivalence between a completely synchronous composition of the blocks, and the LIP-based composition. Every time a new LIP is conceived, it needs to be debugged and then proven correct. Mathematical theorems to establish correctness, though elegant, are error prone, and tedious to create for every new variant of LIPs. In this work, we present validation frameworks for families of LIPs, both for dynamic validation, useful for early debug cycles, and formal verification for formal proof of correctness. This can be a useful framework in the hands of designers trying to create new LIPs or to optimize existing ones for design convergence.

Existing system-level design languages (SLDLs) and frameworks mainly provide a modeling and a simulation framework. However, there is an increasing demand for supporting tools to aid designers in quick and faster design space and architectural exploration. As a result, numerous tools such as integrated development environments (IDEs) and others that help in debugging, visualization, validation, and verification are commonly employed by designers. As with most tools, they are targeted for a specific purpose, making it difficult for designers to possess all desired features from one particular tool. Only public-domain tools can be easily extended or interfaced with other existing tools, which a lot of the existing commercial tools do not promote. Having an extendable framework allows designers to implement their own desirable features and incorporate them into their framework. However, for technology reuse and transfer, it is important to have a tidy infrastructure for interfacing the extension with the framework, such that the added solution is not highly coupled with the environment, making distribution and deployment to other frameworks difficult, if not impossible. This requires a plug-and-play framework where features can be easily integrated. These issues of extendibility, deployment, and the inadequacies in SLDLs and frameworks are tackled by presenting a service-oriented architecture for validating SLDs for SystemC, called CARH, We code name our software systems after famous computer scientists. CARH which uses a variety of open-source technologies such as Doxygen, Apache's Xerces extensible markup language parsers, SystemC, and the adaptive communication environment (ACE) object request broker.

We present an agile formal methodology named eXtreme Formal Modeling (XFM), based on Extreme Programming (XP) concepts to construct abstract models from natural language specifications of complex systems. In particular, we focus on Prescriptive Formal Models (PFMs) that capture the specification of the system under design in a mathematically precise manner. Such models can be used as golden reference models for formal verification, test generation, coverage monitor generation, etc. This methodology for incrementally building PFMs works by adding user stories expressed as LTL formulae gleaned from the natural language specifications, one by one, into the model. XFM builds the models, retaining correctness with respect to incrementally added properties by regressively model-checking all the LTL properties captured theretofore in the model. We illustrate XFM with a graded set of examples consisting of a traffic light controller and a DLX pipeline. To make the regressive model-checking steps feasible with current model-checking tools, we need to control the model size increments at each subsequent step in the process. We therefore analyze the effects of ordering the LTL properties in XFM on the statespace growth rate of the model. We compare three different property-ordering methodologies: ad hoc ordering, property-based ordering, and predicate-based ordering. We experiment on the models of the ISA bus monitor and the arbitration phase of the Pentium Pro bus. We experimentally show and mathematically reason that the predicate-based ordering is the best among these orderings. Finally, we present a GUI-based toolbox that we implemented to build PFMs using XFM.

Growing design sizes and shrinking time to market windows can only be met with drastically increased productivity. One way to obtain this is a smart reuse of intellectual property. This paper presents a methodology for modular design with the help of component abstraction. It describes how imperative components can be transformed into a formal, synchronous description to provide behavioral types to the components. The synchronous composition of these abstracted components helps discover errors in the component composition. The presented methodology is illustrated by the detailed case study of a Finite Impulse Response filter. We transform initial \systemc\ modules into an intermediate static single assignment representation which is used as a basis from which corresponding behavioral types are built.