VIS-v can only work on a strict subset of BLIF-MV although any synthesis-related commands like read_blif and write_blif, are applicable to the full-set of BLIF-MV. If the user generates BLIF-MV files using VL2MV following a certain restriction (See the VIS users' manual for details), the files are guaranteed to be in the subset. However, if BLIF-MV files are generated manually, the user must make sure that the files are in the VIS-v subset. Otherwise, init_verify simply fails, thereby making it impossible to perform the verification.
The restriction we pose is as follows.