Sciweavers

FMCAD
2006
Springer
13 years 8 months ago
Design for Verification of the PCI-X Bus
The importance of re-usable Intellectual Properties (IPs) cores is increasing due to the growing complexity of today's system-on-chip and the need for rapid prototyping. In th...
Haja Moinudeen, Ali Habibi, Sofiène Tahar
FMCAD
2006
Springer
13 years 8 months ago
Enabling Large-Scale Pervasive Logic Verification through Multi-Algorithmic Formal Reasoning
Pervasive Logic is a broad term applied to the variety of logic present in hardware designs, yet not a part of their primary functionality. Examples of pervasive logic include init...
Tilman Glökler, Jason Baumgartner, Devi Shanm...
FMCAD
2006
Springer
13 years 8 months ago
Over-Approximating Boolean Programs with Unbounded Thread Creation
Abstract-- This paper describes a symbolic algorithm for overapproximating reachability in Boolean programs with unbounded thread creation. The fix-point is detected by projecting ...
Byron Cook, Daniel Kroening, Natasha Sharygina
FMCAD
2006
Springer
13 years 8 months ago
Reducing Verification Complexity of a Multicore Coherence Protocol Using Assume/Guarantee
Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Chi...
FMCAD
2006
Springer
13 years 8 months ago
Formal Analysis and Verification of an OFDM Modem Design using HOL
In this paper we formally specify and verify an implementation of the IEEE802.11a standard physical layer based OFDM (Orthogonal Frequency Division Multiplexing) modem using the HO...
Abu Nasser Mohammed Abdullah, Behzad Akbarpour, So...
FMCAD
2006
Springer
13 years 8 months ago
Automatic Generation of Schedulings for Improving the Test Coverage of Systems-on-a-Chip
Claude Helmstetter, Florence Maraninchi, Laurent M...
FMCAD
2006
Springer
13 years 8 months ago
An Integration of HOL and ACL2
We describe a link between the ACL2 and HOL mechanical proof assistants that enables the strengths of each system to be deployed smoothly within a single formal development. Severa...
Michael J. C. Gordon, James Reynolds, Warren A. Hu...
FMCAD
2006
Springer
13 years 8 months ago
Liveness and Boundedness of Synchronous Data Flow Graphs
Synchronous Data Flow Graphs (SDFGs) have proven to be suitable for specifying and analyzing streaming applications that run on single- or multi-processor platforms. Streaming appl...
Amir Hossein Ghamarian, Marc Geilen, Twan Basten, ...
FMCAD
2006
Springer
13 years 8 months ago
Ario: A Linear Integer Arithmetic Logic Solver
Ario is a solver for systems of linear integer arithmetic logic. Such systems are commonly used in design verification applications and are classified under Satisfiability Modulo T...
Hossein M. Sheini, Karem A. Sakallah