Describing Designs for VIS

VIS operates on an intermediate format called BLIF-MV, which is an extension of BLIF, the intermediate format for logic synthesis accepted by SIS [ 4 ]. VIS includes a stand-alone compiler from Verilog to BLIF-MV, called VL2MV [3 ], which supports a synthesizable subset of Verilog. VL2MV extracts a set of interacting finite state machines that preserves the behavior of the source Verilog program defined in terms of simulated results. Two new features have been added to Verilog:

1.

Nondeterminism. A nondeterministic construct, $ND, has been added to specify nondeterminism on wire variables; this is the only legal way to introduce nondeterminism in VIS. Internally, $ND introduces pseudo-inputs which can non-deterministically take any allowed value.

2.

Symbolic variables. Sometimes it is desirable to specify and examine the value of variables symbolically, rather than having to explicitly encode them. VL2MV extends Verilog to allow symbolic variables using an enumerated type mechanism similar to the one available in the C programming language.

Currently, a translator from a subset of VHDL to BLIF-MV is being developed and a path from Esterel to BLIF-MV is available through the POLIS system at Berkeley.