Repository files navigation

This is an EDA tool for clock domain crossing verification, currently at anearly state of development and not yet available for use (please wait for arelease). More information on the tool is available onhttps://xprova.net.

• java 8
• Maven
• Yosys

Until I document the various functions and capabilities of the tool properly Iwill list the commands currently supported here with brief explanationsfollowing cookbook principles.

Xprova is a command line tool, when launched it should print the followingbanner and prompt:

 __  __ \ \/ /_ __  _ __ _____   ____ _  \  /| '_ \| '__/ _ \ \ / / _` |  /  \| |_) | | | (_) \ V / (_| | /_/\_\ .__/|_|  \___/ \_/ \__,_|      |_|Type :l for a list of available commands or :q to quit>>

The first step is to always load a gate library by runningload_lib file.lib. The library must be a verilog file containing module headers andinput/output statements (to specify port directions), for example:

moduleAND (y, a, b);input a, b;output y;endmodulemoduleNOT (y, a);input a;output y;endmodule

Library modules may not instantiate other modules.

The tool must also be told which modules in the library are flip-flops(currently there is no automated way of inferring this). Flip-flop modules aredefined by running:

def_ff QDFFRSBX1 CK RS D

The first argument ofdef_ff is the flip-flop module name and the rest areclock port, reset port and data port respectively.

To list existing flip-flop definitions runlist_ff and to clear them runclear_ff.

To load a verilog netlist, run:

read_verilog design.v

If the file contains multiple modules then the first will be loaded and therest ignored. If you'd like to specify which module to load use:

read_verilog -m top design.v

Note: the tool supports flattened netlists only atm. Instantiations of modulesthat are not defined in the library will cause an Exception to be thrown.

The command to do this isaugment_netlist.

Simply runwrite_verilog augmented.v

The tool can output various graph representations of the netlist using thecommandexport_dot.

export_dot output.dot# to create a graph of nets and gates only (ignore flip-flops):export_dot --type=ng output.dot# to create a graph of gates and flops only (ignore nets):export_dot --type=gf output.dot# to create a graph of flip flops only:export_dot --type=f output.dot# so basically the option --type can take any char combination of "ngf"# to omit verticess (useful to remove reset and clock connections):export_dot --ignore-vertices=rst,clk1,clk2 output.dot# to omit edges (ditto):export_dot --ignore-edges=SB,RB,CK# to combine multiple vertices into one:export_dot --combine=add[0],add[1],add[2] output.dot