Auxiliary state machines and auxiliary functions: constructs for extending AMS assertions

Abstract

As research on developing assertion languages for the AMS domain gains in momentum, it is increasingly being felt that extensions of existing assertion languages like PSL and SVA into the AMS domain are not adequate for expressing the analog design intent. This is largely due to the intricacy of the analog behavioral intent which cannot be captured purely in terms of logic. In this paper we show that by using auxiliary forms of formal specifications such as abstract state machines and real valued functions as references for AMS assertions, it becomes possible to model complex AMS behavioral properties. This approach leverages the growing adoption of AMS behavioral modeling in the industry. The paper also shows that the use of auxiliary state machines allows us to separate out the scope of different analog assertions leading to significant performance gains in the assertion checking overhead.