Hybrid, Incremental Assertion-Based Verification for TLM Design Flows
Found in: IEEE Design and Test of Computers
By Nicola Bombieri, Franco Fummi, Graziano Pravadelli, Andrea Fedeli
Issue Date:March 2007
pp. 140-152
Transaction-level modeling (TLM) has been proposed as the leading strategy to address the ever-increasing complexity of digital systems. However, its introduction brings a new challenge for designers and verification engineers. Because no tools are availab...

Predicting Timeliness of Reactive Systems under Flexible Scheduling
Found in: Autonomous Decentralized Systems, International Symposium on
By Giacomo Bucci, Andrea Fedeli, Enrico Vicario
Issue Date:April 2003
pp. 125
A modeling and validation approach extending the formalism of Time Petri Nets for the analysis of real time systems with flexible scheduling capabilities is introduced. The new formalism is called AdaptiveTPNs. State space analysis of the model supports ex...

Properties Incompleteness Evaluation by Functional Verification
Found in: IEEE Transactions on Computers
By Andrea Fedeli, Franco Fummi, Graziano Pravadelli
Issue Date:April 2007
pp. 528-544
Verification engineers cannot guarantee the correctness of the system implementation by model checking if the set of proven properties is incomplete. However, the use of model checking lacks widely accepted coverage metrics to evaluate the property complet...

On PSL Properties Re-use in SoC Design Flow Based on Transaction Level Modeling
Found in: Microprocessor Test and Verification, International Workshop on
By Nicola Bombieri, Andrea Fedeli, Franco Fummi
Issue Date:November 2005
pp. 127-132
In this paper we present some key concepts concerning the Properties Specification Language (PSL) utilization in a system level verification flow for System on Chip (SoC) designs. As Transaction Level Modeling (TLM) is the defacto reference model for SoC d...

Timed State Space Analysis of Real-Time Preemptive Systems
Found in: IEEE Transactions on Software Engineering
By Giacomo Bucci, Andrea Fedeli, Luigi Sassoli, Enrico Vicario
Issue Date:January 2004
pp. 97-111
<p><b>Abstract</b>—A modeling notation is introduced which extends Time Petri Nets with an additional mechanism of resource assignment making the progress of timed transitions be dependent on the availability of a set of preemptable resou...

On the Use of a High-Level Fault Model to Check Properties Incompleteness
Found in: Formal Methods and Models for Co-Design, ACM/IEEE International Conference on
By Franco Fummi, Graziano Pravadelli, Andrea Fedeli, Umberto Rossi, Franco Toto
Issue Date:June 2003
pp. 145
The use of model checking to validate descriptions of digital systems lacks a coverage metrics. The set of proven properties can be incomplete, thus not guaranteeing the behavioral checking completeness of the digital system implementation with respect to ...

Concrete Impact of Formal Verification on Quality in IP Design and Implementation
Found in: Quality Electronic Design, International Symposium on
By Umberto Rossi, Andrea Fedeli, Marco Boschini, Franco Toto
Issue Date:March 2001
pp. 38
The application of formal methods to the logic verification of electronic circuits is meant for increasing the coverage obtained by the traditional verification techniques. This concept is quite popular in the design community but requires some guidelines ...