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...
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...
Abstract-- This paper describes a symbolic algorithm for overapproximating reachability in Boolean programs with unbounded thread creation. The fix-point is detected by projecting ...
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...
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...
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, ...
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...