Wu's Method Based Temporal Assertions Checking for SEREs Properties

摘要

In this paper we propose an approach using Wu's Method to perform SEREs assertion verification for synchronous digital circuit systems. We define a constrained simple subset of SEREs so that an efficient polynomial modeling mechanism for both circuit descriptions and assertions can be applied. We present an algorithm framework based on algebraic representations using the characteristic set of polynomial system. Case studies show that computer algebra can provide canonical symbolic representations for PSL temporal assertions verification and Wu's Method based approach can act as a novel solver engine from a theoretical viewpoint.