URL https://opencores.org/ocsvn/dblclockfft/dblclockfft/trunk

Subversion Repositories dblclockfft

[/] [dblclockfft/] [trunk/] [bench/] [formal/] [README.md] - Blame information for rev 36

Go to most recent revision | Details | Compare with Previous | View Log


This directory contains several SymbiYosys scripts useful for
formally verifying parts and pieces of the design.  Admittedly,
the entire design has yet to be formally verfified, however many
components have been verified successfully.  These include:
 
- The butterflies, both the hardware enabled butterflies and the
  soft multiplies.
 
- 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.

Line No.	Rev	Author	Line
1	36	dgisselq	`This directory contains several SymbiYosys scripts useful for`
2			`formally verifying parts and pieces of the design. Admittedly,`
3			`the entire design has yet to be formally verfified, however many`
4			`components have been verified successfully. These include:`
5
6			`- The butterflies, both the hardware enabled butterflies and the`
7			`soft multiplies.`
8
9			`- The penultimate (4-pt) stage of the FFT`
10
11			`- The final stage (2-pt) of the FFT`
12
13			`- The bitreverse`
14
15			`My intention is not to place formal properties into the repository.`
16			`Within the [defaults.h](../../sw/defaults.h) there's a`
17			``formal_property_flag`` used for controlling whether or not the
18			`formal properties are included into the RTL files.`

Browse

Tools

Subversion Repositories dblclockfft

[/] [dblclockfft/] [trunk/] [bench/] [formal/] [README.md] - Blame information for rev 36