All these concepts are implemented in a prototype tool. The scope of the proposed technique is significantly improved by adding to PSL both a formal and a practical support for auxiliary global and local variables, which are compelling in higher level specifications. A specific method for monitoring communication activities at a high level of abstraction is also described. An effective technique for the construction of checker modules from PSL properties is proposed : this technique for SystemC TLM is inspired from a pioneering approach for RTL. While most existing ABV solutions are restricted to the register transfer level (RTL), the work of this thesis attempts to overcome some limitations by developing an actual ABV solution for the transaction level modeling (TLM) in SystemC.
#Formal property verification verification
In this context, Assertion-Based Verification (ABV) has widely gained acceptance over the recent years : following this approach, temporal properties expressed using languages such as PSL or SVA specify the expected behavior of the design. Ensuring the correct behavior of each component, as well as validating the behavior of the whole system, is both a compelling and painful task. This development leads to Systems-on-Chip incorporating a combination of components with highly heterogeneous features. Moreover, electronic circuits have become widespread elements in many different areas.
Over the last years, the growing of electronic circuit complexity has experienced a tremendous evolution.
0 kommentar(er)
