Logic of constraints: a quantitative performance and functional constraint formalism

In the era of billion-transistor design, it is critical to establish effective verification methodologies from the system level, all the way down to the implementations. In this paper, we introduce logic of constraints (LOC), a logic that is particularly suited to express quantitative performance constraints as well as functional constraints. We analyze the expressiveness of LOC and show that it is important and different from linear temporal logic, upon which traditional hardware assertion languages (e.g., PSL and OpenVera) are based. We propose an automatic simulation trace checking/runtime monitoring methodology that can be used to verify system designs very efficiently. Since a subset of LOC is decidable, we also discuss the formal verification approach for LOC formulas. Through several industrial case studies, we demonstrate the usefulness of the LOC formalism and the corresponding simulation and verification approach at the higher transaction level of abstraction.