The Vis FAQ


From: Roderick Bloem 
Subject: VIS Frequently Asked Questions (FAQ)
Date: 6 April 2000
Organization: University of Colorado at Boulder
Summary: Questions and answers having to do with Vis
Keywords: VIS FAQ

FAQ: Introduction

This is a list of frequently asked questions (FAQ) about Vis 1.4 with answers. It is relatively new, and hence not very complete. 

Questions

  • General Questions
    • 1. What is Vis?
    • 2. Where do I get Vis?
    • 3. Where do I get Vis documentation?
    • 4. How can I get more help?
  • Compilation Problems
    • 5. I cannot compile vl2mv on my Linux machine.
  • Translation of hardware description languages
    • 6. My Verilog description is translated incorrectly by vis.
    • 7. How do I read a VHDL file into Vis?
  • Errors from Vis
    • 8. Node is not driven only by latches and constants
    • 9. I found a bug!
  • Performance
    • 10. The init_verify or build_partition_mdds command does not complete. What do I do?
    • 11. Vis is too slow / does not finish. What do I do?
    • 12. How do I interpret the output of the print commands?

Answers

General Questions

1. What is Vis?

See What is Vis.

2. Where do I get Vis?

At http://vlsi.colorado.edu/~vis, which is the Vis home page.

3. Where do I get Vis documentation?

From the Vis home page there are two links. One link is to User Documentation. The user documentation is meant for the end user. It discusses vis commands, has an overview and a tutorial paper, a user's manual and manuals for BLIF, BLIF-MV, CTL, vl2mv and Xsimv. The Programmer Documentation, is meant for people developing code in Vis. It describes the internal functions.

4. Where do I get more help?

This FAQ is still young (started in December 99), and many questions aren't anwered here. If you cannot find your answer, please send us mail at vis-users@colorado.edu. We're happy to help. Tell us which version of vis you are using, and send along the following:

  1. The verilog file,
  2. the blif-mv file,
  3. any input you typed, and
  4. the output you received from vis.

Compilation Problems

5. I cannot compile vl2mv on my Linux machine.

Get a vl2mv executable from ftp://vlsi.colorado.edu/pub/vl2mv/new/executables/vl2mv.linux.

Translation of hardware description languages

6. My Verilog description is translated incorrectly by vis.

Please report your problem to the adress mentioned in Question 4. If possible, find the smallest possible description that still exhibits the bug. In your mail, include the version of vis you are using, your original verilog file, the blif-mv file that vl2mv generated, the results of vis (from the command line), and the results you had expected.

You can obtain a blif-mv translation by running vl2mv from the shell command line: vl2mv file.v will produce a file called file.mv.

There are many problems with vl2mv, the verilog to blif-mv translator. We are not going to solve these problems, but here is a discussion on how to write Verilog for vl2mv.

7. How do I read a VHDL file into Vis?

There is no support for VHDL, and none is planned. If you have the Synopsys Design Compiler, you can use it to translate VHDL to Verilog. You can also have it output EDIF, and translate EDIF to blif using edif2blif. A similar route exists using Altera MaxPlusII.

Errors from Vis

8. Node S is not driven only by latches and constants

Vis gives me the following error:
** mc error: error in parsing Atomic Formula:
Node S found in the support of node S.
Node S is not driven only by latches and constants.

The problem is that signal S is an input. That is not allowed.

To bypass this restriction, create an extra latch that latches your input, and use the latch in your formula. This changes your input-output language by shifting the input by one timestep, but typically that is not a problem. An example follows.

Suppose we have this verilog

module simple(clk, in);
    input clk;
    input in;

    reg   latch;

    initial latch = 0;

    always @(posedge clk)
      latch = in;

endmodule
If we wish to see that latch follows input with delay 1, we can use this formula. this formula:
AG(in = 1 -> AX latch = 1);
things will not work because in is an input. We need to change the verilog and the formula as follows.
module simple2(clk, in);
    input clk;
    input in;

    reg   latch;
    reg   inlatched;
    
    initial begin
	latch = 0;
	inlatched = 0;
    end
    
    always @(posedge clk)
      inlatched = in;

    always @(posedge clk)
      latch = inlatched;

endmodule
AG(inlatched = 1 -> AX latch = 1);

9. I found a bug!

Please tell us! See question 4. We try to produce high-quality code, and a core dump or another bug will certainly get our attention.

Performance

10. The init_verify or build_partition_mdds command does not complete. What do I do?

There are multiple possible reasons. One thing you should try is to enable dynamic variable reordering before calling build_partition_mdds. If you use init_verify, replace it by flt; so; dvo -e sift -v1; part. If this doesn't do it, see question 11.

11. Vis is too slow / does not finish. What do I do?

There are many possible explanations. You may just have a circuit that is too big. Certain constructs, such as barrel shifters and multipliers, are known to be very hard. Avoid these designs.

One thing to try is to set the datasize limit. Before starting vis, enter the following on the command line: limit datasize xxx where xxx is about 80% of the memory you have in your machine. This will tell Cudd (the underlying BDD package) that it is allowed to use all this memory. Typically, this will improve performance.

Vis has extremely poor memory locality. Almost as soon as it uses up the physical memory in your machine, it will start thrashing, and performance will become negligible. Virtual memory is of little use.

12. How do I interpret the output of the print commands?

Read this discussion.

Contact 
©2002-2018 U.C. Regents