URL
https://opencores.org/ocsvn/dblclockfft/dblclockfft/trunk
Show entire file |
Details |
Blame |
View Log
| Rev 36 |
Rev 40 |
| Line 1... |
Line 1... |
This directory contains several SymbiYosys scripts useful for
|
This directory contains several SymbiYosys scripts useful for formally verifying parts and pieces
|
formally verifying parts and pieces of the design. Admittedly,
|
of the design. While the top level of the design has yet to be formally verified, scripts are
|
the entire design has yet to be formally verfified, however many
|
present for verifying all of the other components--save the [long binary multiply,
|
components have been verified successfully. These include:
|
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.
|
|
|
- The butterflies, both the hardware enabled butterflies and the
|
Within the [defaults.h](../../sw/defaults.h) there's a ``formal_property_flag`` used for
|
soft multiplies.
|
controlling whether or not the formal properties are included into the RTL files.
|
|
|
- The penultimate (4-pt) stage of the FFT
|
|
|
|
- The final stage (2-pt) of the FFT
|
|
|
|
- The bitreverse
|
|
|
|
My intention is not to place formal properties into the repository.
|
|
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.
|
|
controlling whether or not the formal properties are included into the RTL files.
|
|
© copyright 1999-2024
OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.