Footnotes
 

 

...
Circuits with combinational cycles are legal in BLIF-MV, but currently they are not processed by VIS.
...
VL2MV can also extract quantitative timing information from a timed Verilog program, producing BLIF-MVT, based on timed automata, that is an extension of BLIF-MV with timing constructs [3]. Since verification with quantitative timing is not handled in the current version of VIS, this feature is of no further interest here.
...
These gates generate some output from the set of pre-specified outputs.
...
A formula that contains any temporal modality (, , , ) without an associated path quantifier (, ) is not a legal CTL formula.
...
``Weak until'' is when holds forever, i.e., is not required to hold at some state in the future.
...
It is possible to show two transition systems that recognize the same language, of which one satisfies , and the other does not.
...
Whenever a hierarchy is reinitialized, the option flatten_hierarchy -b can be used safely for efficiency.
...
One would need a flattening routine different from the one which starts the verification flow already in VIS, and such a routine to flatten for synthesis is not yet available.

Yuji Kukimoto
Tue Feb 6 11:58:14 PST 1996
Contact 
©2002-2018 U.C. Regents