Assets & Tools

The ICE Laboratory was set up to promote synergy between the technological innovation of Industry 4.0 and the education and research centers located in the Verona area. The facility is part of the IT excellence project, which was awarded 8 million euro by the Italian Ministry of Education, Universities, and Research. The project involves creating prototypes that can be used in production lines with the integration of augmented reality. 

HIFSuite: Tools for HDL code conversion and manipulation

HIFSuite is a set of tools and application programming interfaces (APIs) that provide support for modeling and verification of HW/SW systems. The core of HIFSuite is the HDL Intermediate Format (HIF) language upon which a set of front-end and back-end tools have been developed to allow the conversion of HDL code into HIF code and vice versa. HIFSuite allows designers to manipulate and integrate heterogeneous components implemented by using different hardware description languages (HDLs). Moreover, HIFSuite includes tools, which rely on HIF APIs, for manipulating HIF descriptions in order to support code abstraction/refinement and post-refinement verification. Moreover, through the manipulation tools it is possible to inject different types of faults to generate faulty models.

Initial publication on IEEEXplore.

EDACurry - The Unified Mixed-signal Netlist Parser

There are plentiful successors of SPICE language for describing transistor-level designs. For most of them, the semantic match those of SPICE, and only the syntax is changed. Others instead provide more default models or analysis tools.

The EDACurry library is based on a shared semantic for reading, writing, or manipulating transistor-level designs. The ultimate goal of the framework is: reading an input design written in a specific syntax and then allowing to write the same design in another syntax. First, the input description is parsed by a language-specific front-end which turns it into an in-memory abstract syntax tree that follows the common semantic. Then, the in-memory description can be subject to different user-defined manipulations built on top of a series of API or visitor/listener classes. Finally, the description goes through the desired back-end, transforming the in-memory description into the target transistor-level language.

Moreover, exploiting the JSON back-end it is possible to print in the output the in-memory description, subsequently, it is possible to read this JSON description through the appropriate front-end that allows populating automatically the in-memory description. This series of operations allows obtaining pipelines of tools to perform structured manipulations of transistor-level netlists. In addition, exploiting the JSON description produced through the appropriate back-end it is possible, through a Python script that transforms the file in DOT language (compatible with the GrapViz library) to visualize the in-memory description as a tree.

Initial publication on IEEEXplore.

The Contract-based Heterogeneous Analysis and System Exploration (CHASE) framework is a requirement engineering framework combining specification and modeling formalisms with rigorous verification and synthesis procedures relying on A/G contracts.
CHASE also provides interfaces for the designers to implement novel design tools and methodologies.

Its main component is the representation core library, which provides a set of classes to represent requirements, components, and system models in terms of A/G contracts.Contracts are then mathematical models with rigorous composition rules that provide mechanisms to analyze system behaviors, validate design requirements, and develop system components in a modular and hierarchical way. The CHASE library supports the representation of A/G contracts expressed in propositional logic or Linear Temporal Logic (LTL) and implements the operations defined by the contract algebra. Thus, it allows exploiting the compositionality and rigor provided by A/G contracts and their algebra to automate verification and synthesis tasks. The library also supports the representation of Signal Temporal Logic and Metric Temporal Logic, enabling the use of the most appropriate formalism for the specification of the design requirements. Finally, CHASE supports the representation of arithmetic constraints on real numbers, dynamical systems in the state space, and probability distributions to specify stochastic components and probabilistic constraints.

A set of methods allow accessing the functionalities of the core library to manipulate the design representations. These methods are exported to designers by C++ and Python Application Programming Interfaces (APIs). Design methodologies can be implemented on top of CHASE by writing tools that exploit these APIs.

Front-end and back-end tools can also be developed on top of the CHASE library. Front-end tools are used to aid the formalization of the requirements, usually expressed in semi-formal languages, by encoding them in the formal constructs of the core library. Back-end tools interface the internal representation provided by the core library to external solvers.

Initial publication on IEEExplore.