On simulation-based probabilistic model checking of mixed-analog circuits