Subversion Repositories dblclockfft

This directory contains several SymbiYosys scripts useful for formally verifying parts and pieces
of the design.  While the top level of the design has yet to be formally verified, scripts are
present for verifying all of the other components--save the [long binary multiply,
longbimpy](../../rtl/longbimpy.v).  The properties within the [long binary
multiply](../../rtl/longbimpy.v) only proves certain properties of the binary multiply.  The [full
proof](../cpp/mpy_tb.cpp) is done by exhaustion via Verilator in the [bench/cpp](../cpp) directory.

Within the [defaults.h](../../sw/defaults.h) there's a ``formal_property_flag`` used for
controlling whether or not the formal properties are included into the RTL files.