Workspaces ---- apbd asves asvpapers bear blast caltrop cases concurrency cosi dif diva dopcenter dopresence dopsysadmin eecsx44 elab embedded embeddedadmin giotto hyinfo m2t2 mescal metropolis mica mobies msgadmin murieh mvsis nephest ransom recons robosysadmin savg sec seminar smartnets video webmaster

Next: About this document Up: BLIF-MV Previous: Semantics The VIS-v Subset of BLIF-MV 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. The only allowable nondeterministic tables are pseudo-input tables, which are no-input, single-output tables which generate more than one output nondeterministically. Note that one can always transform any BLIF-MV file to its equivalent BLIF-MV file in the VIS-v subset by determinizing all intermediate nondeterministic tables by adding pseudo-inputs. Stephen Anthony Edwards Fri Nov 22 19:07:27 PST 1996

Contact

©2002-2018 U.C. Regents