Model Extraction for Designs Based on Switches for Formal Verification