We present a novel approach to functional verification of mixed signal designs by symbolic manipulations of Multiplicative binary moment diagrams (*BMDs). *BMDs effectively represent and manipulate both algebraic and Boolean operations, which makes them suitable to handle the features of mixed signal systems. A formal model of the structural implementation of a synthesized design is extracted from the sized component netlist produced by the synthesis tool, in terms of characteristic behavior of the components and various voltage and current laws. For the synthesized implementation to be correct, it must imply formal models of user given behavior specification and other interesting properties. Circuit implementation and expected behavior are both modeled in *BMDs and the expected logical relation between them is proven.