Abstract-- Analog and Mixed Signal (AMS) designs are important integrated systems that link digital circuits to the analog world. Following the success of PSL verification methodologies, recent research suggested extending PSL to support AMS systems. However, PSL has been defined initially to formalize properties about logical signals using models such as automata. In fact, the presence of continuous signals in AMS systems and the continuous notion of time are the main obstacles in adopting PSL. In this paper, we propose an approach to verify PSL properties for a class of AMS systems. Our approach is based on modeling the AMS design in terms of a System of Recurrence Equations (SRE). Then, we define an Assertion Based Verification method using the symbolic trace of SRE.
Ghiath Al Sammane, Mohamed H. Zaki, Zhi Jie Dong,