Publications

Publications avec comités de relecture

DATICS-IMECS'11 Extracting Logical Formulae that Capture the Functionality of SystemC Designs
Nicolas Vallée, Bruno Monsuez, Vladimir-Alexandru Paun
pdf Abstract:
Object-oriented hardware design languages like SystemC have become very popular to co-design hardware and software systems. Such designs are classically translated into a transition system in order to verify a specification with model-checkers. However, compositionnality and parametricity of SystemC components complicate their translations into finite transition systems. Processing analysis of high-level designs occurs early in the design flow and aims to greatly reduce the correction costs of eventual errors. In this paper, we propose a formal method to statically analyze SystemC designs. Our approach consists in extracting a logical formula representing the behavior of the system in order to avoid combinatorial explosion. This method combines a symbolic execution of SystemC code to infer logical formulae representing its behavior and a generalization phase of these inferred logical properties.
DATICS-IMECS'10 A Formal Model Of SystemC Components Using Fractal Hypergraphs
Nicolas Vallée, Bruno Monsuez
pdf Award: Certificate of Merit
Abstract:
In this paper, we introduce a new mathematical structure: fractal hypergraph. Due to the hierarchical and compositional nature of fractal hypergraphs, representations based on fractal hypergraphs can capture and abstract the object-oriented nature of SystemC. We propose a formal semantics of SystemC components based on fractal hypergraphs that has already be used in a formal debugger of SystemC components.
DATICS-ICC'08 On the design of a Formal Debugger for System Architecture
Bruno Monsuez, Franck Védrine, Nicolas Vallée
pdf Abstract:
System level design helps alleviate much of the burden of usual RTL level design except verification. Functional verification of system architecture may first seem easier at the higher level of abstraction. In fact, insight on fundamental aspects of semantics of system level design and impact on lower levels of abstraction makes it much harder. Formal verification has received till now little attention for functional verification of system architecture. However, formal verification may provide great benefits to the system level designers. In this paper, starting from the experiments we have conducted with analyzing and verifying SystemC models using formal verification techniques, we describe what a potentially very useful approach to build a formal debugger to verify system architectures designed using a modern system model language like SystemC or SystemVerilog.

Publications invitées

CISST'09 How an "Incoherent Behavior" inside generic hardware component characterizes functional errors ?
Bruno Monsuez, Franck Védrine, Micaela Mayero, Nicolas Vallée
pdf Abstract:
Detecting functional errors on generic hardware components is often a complex task. This task becomes more complex in a componentwise approach when analyzing components without their embedded context that is the entire system description. In this paper, we propose a methodology that successfully detects just from the component's description a pure functional error that neither extensive tests nor formal methods could find.