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

Subversion Repositories dblclockfft

Compare Revisions

  • This comparison shows the changes necessary to convert path 
    /
    from Rev 39 to Rev 40
    ↔ Reverse comparison
  •

Rev 39 → Rev 40

/dblclockfft/trunk/bench/formal/.gitignore
1,5 → 1,7
bimpy
bitreverse
laststage
longbimpy
qtrstage
hwbfly_one
hwbfly_two
13,3 → 15,10
butterfly_ck3_r0
butterfly_ck3_r1
butterfly_ck3_r2
windowfn_cover
windowfn_proof
fftstage_s2
fftstage_s3
fftstage_s4
fftstage_s5
fftstage_s6
/dblclockfft/trunk/bench/formal/Makefile
0,0 → 1,84
################################################################################
##
## Filename: bench/formal/Makefile
##
## Project: A General Purpose Pipelined FFT Implementation
##
## Purpose: Runs all of the SymbiYosys enabled formal proofs. Requires
## the formal code within the various modules to be enabled.
##
## Creator: Dan Gisselquist, Ph.D.
## Gisselquist Technology, LLC
##
################################################################################
##
## Copyright (C) 2018, Gisselquist Technology, LLC
##
## This file is part of the general purpose pipelined FFT project.
##
## The pipelined FFT project is free software (firmware): you can redistribute
## it and/or modify it under the terms of the GNU Lesser General Public License
## as published by the Free Software Foundation, either version 3 of the
## License, or (at your option) any later version.
##
## The pipelined FFT project is distributed in the hope that it will be useful,
## but WITHOUT ANY WARRANTY; without even the implied warranty of
## MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser
## General Public License for more details.
##
## You should have received a copy of the GNU Lesser General Public License
## along with this program. (It's in the $(ROOT)/doc directory. Run make
## with no target there if the PDF file isn't present.) If not, see
## <http://www.gnu.org/licenses/> for a copy.
##
## License: LGPL, v3, as defined and found on www.gnu.org,
## http://www.gnu.org/licenses/lgpl.html
##
##
################################################################################
##
##
TARGETS := bimpy longbimpy fftstage hwbfly butterfly qtrstage laststage bitreverse
.PHONY: $(TARGETS)
all: bimpy longbimpy hwbfly fftstage qtrstage laststage bitreverse # butterfly
 
bimpy:
sby -f bimpy.sby
 
longbimpy:
sby -f longbimpy.sby
 
fftstage:
sby -f fftstage.sby
 
hwbfly:
sby -f hwbfly.sby
 
butterfly:
sby -f butterfly.sby
 
qtrstage:
sby -f qtrstage.sby
 
laststage:
sby -f laststage.sby
 
bitreverse:
sby -f bitreverse.sby
 
windowfn:
sby -f windowfn.sby
 
clean:
rm -rf bimpy/ longbimpy/
rm -rf bitreverse/
rm -rf butterfly_ck1/
rm -rf butterfly_ck2_r0/
rm -rf butterfly_ck2_r1/
rm -rf butterfly_ck3_r0/
rm -rf butterfly_ck3_r1/
rm -rf butterfly_ck3_r2/
rm -rf fftstage_s2/ fftstage_s3/ fftstage_s4/ fftstage_s5/ fftstage_s6/
rm -rf hwbfly_one/ hwbfly_two/ hwbfly_three/
rm -rf laststage/ qtrstage/
rm -rf windowfn_cover/ windowfn_proof/
/dblclockfft/trunk/bench/formal/README.md
1,18 → 1,9
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:
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.
 
- 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.
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.
/dblclockfft/trunk/bench/formal/abs_longbimpy.v
0,0 → 1,147
////////////////////////////////////////////////////////////////////////////////
//
// Filename: ../rtl/abs_longbimpy.v
//
// Project: A General Purpose Pipelined FFT Implementation
//
// Purpose: A portable shift and add multiply, built with the knowledge
// of the existence of a six bit LUT and carry chain. That knowledge
// allows us to multiply two bits from one value at a time against all
// of the bits of the other value. This sub multiply is called the
// bimpy.
//
// For minimal processing delay, make the first parameter the one with
// the least bits, so that AWIDTH <= BWIDTH.
//
//
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2018, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of the GNU General Public License as published
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
// for more details.
//
// You should have received a copy of the GNU General Public License along
// with this program. (It's in the $(ROOT)/doc directory, run make with no
// target there if the PDF file isn't present.) If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License: GPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/gpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype none
//
module longbimpy(i_clk, i_ce, i_a_unsorted, i_b_unsorted, o_r);
parameter IAW=8, // The width of i_a, min width is 5
IBW=12, // The width of i_b, can be anything
// The following three parameters should not be changed
// by any implementation, but are based upon hardware
// and the above values:
OW=IAW+IBW; // The output width
localparam AW = (IAW<IBW) ? IAW : IBW,
BW = (IAW<IBW) ? IBW : IAW,
LUTB=2, // How many bits we can multiply by at once
TLEN=(AW+(LUTB-1))/LUTB; // Nmbr of rows in our tableau
input wire i_clk, i_ce;
input wire [(IAW-1):0] i_a_unsorted;
input wire [(IBW-1):0] i_b_unsorted;
output reg [(AW+BW-1):0] o_r;
 
//
// Swap parameter order, so that AW <= BW -- for performance
// reasons
wire [AW-1:0] i_a;
wire [BW-1:0] i_b;
generate if (IAW <= IBW)
begin : NO_PARAM_CHANGE
assign i_a = i_a_unsorted;
assign i_b = i_b_unsorted;
end else begin : SWAP_PARAMETERS
assign i_a = i_b_unsorted;
assign i_b = i_a_unsorted;
end endgenerate
 
`ifndef FORMAL
// This file should only be used in a formal context.
// The following line should therefore yield a syntax error
assert(0);
`endif
 
reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge i_clk)
f_past_valid <= 1'b1;
 
reg [AW-1:0] f_past_a [0:TLEN+1];
reg [BW-1:0] f_past_b [0:TLEN+1];
 
initial f_past_a[0] = 0;
initial f_past_b[0] = 0;
always @(posedge i_clk)
if (i_ce)
begin
f_past_a[0] <= i_a;
f_past_b[0] <= i_b;
end
 
genvar k;
 
generate for(k=0; k<TLEN+1; k=k+1)
begin
initial f_past_a[k+1] = 0;
initial f_past_b[k+1] = 0;
always @(posedge i_clk)
if (i_ce)
begin
f_past_a[k+1] <= f_past_a[k];
f_past_b[k+1] <= f_past_b[k];
end
end endgenerate
 
// abs_mpy #(.AW(AW), .BW(BW)) thempy(f_past_a[TLEN+1], f_past_b[TLEN+1], o_r);
(* anyseq *) reg [AW+BW-1:0] result;
wire [AW+BW-1:0] f_neg_a, f_neg_b;
 
assign f_neg_a = - {{(BW){f_past_a[TLEN+1][AW-1]}}, f_past_a[TLEN+1]};
assign f_neg_b = - {{(AW){f_past_b[TLEN+1][BW-1]}}, f_past_b[TLEN+1]};
 
always @(*)
if (f_past_a[TLEN+1] == 0)
assume(result == 0);
else if (f_past_b[TLEN+1] == 0)
assume(result == 0);
else if (f_past_a[TLEN+1] == 1)
begin
assume(result[BW-1:0] == f_past_b[TLEN+1]);
assume(result[AW+BW-1:BW] == {(AW){f_past_b[TLEN+1][BW-1]}});
end else if (f_past_b[TLEN+1] == 1)
begin
assume(result[AW-1:0] == f_past_a[TLEN+1]);
assume(result[AW+BW-1:AW] == {(BW){f_past_a[TLEN+1][AW-1]}});
end else if (&f_past_a[TLEN+1])
assume(result == f_neg_b);
else if (&f_past_b[TLEN+1])
assume(result == f_neg_a);
else
assume(result[AW+BW-1] == (f_past_a[TLEN+1][AW-1]
^f_past_b[TLEN+1][BW-1]));
 
 
always @(*)
o_r = result;
endmodule
/dblclockfft/trunk/bench/formal/abs_mpy.v
2,7 → 2,7
//
// Filename: abs_mpy.v
//
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
// Project: A General Purpose Pipelined FFT Implementation
//
// Purpose: This code has been modified from the mpyop.v file so as to
// abstract the multiply that formal methods struggle so hard to
/dblclockfft/trunk/bench/formal/bimpy.sby
0,0 → 1,13
[options]
mode prove
depth 5
 
[engines]
smtbmc
 
[script]
read_verilog -formal -DLONGBIMPY bimpy.v
prep -top bimpy
 
[files]
../../rtl/bimpy.v
/dblclockfft/trunk/bench/formal/butterfly.sby
4,20 → 4,20
ck2_r1
ck3_r0
ck3_r1
ck3_r2
 
[options]
mode prove
depth 30
depth 35
 
[engines]
smtbmc
smtbmc boolector
 
[script]
read_verilog -formal -DHWBFLY abs_mpy.v
read_verilog -formal -DHWBFLY convround.v
read_verilog -formal -DHWBFLY longbimpy.v
read_verilog -formal -DHWBFLY bimpy.v
read_verilog -formal -DHWBFLY butterfly.v
read -formal -DBUTTERFLY convround.v
read -formal -DBUTTERFLY bimpy.v
read -formal -DBUTTERFLY longbimpy.v
read -formal -DBUTTERFLY butterfly.v
 
# While I'd love to change the width of the inputs and the coefficients,
# doing so would adjust the width of the firmware multiplies, and so defeat
31,12 → 31,10
ck3_r0: chparam -set CKPCE 3 -set CWIDTH 16 -set IWIDTH 12 -set F_CHECK 0 butterfly
ck3_r1: chparam -set CKPCE 3 -set CWIDTH 18 -set IWIDTH 14 -set F_CHECK 1 butterfly
ck3_r2: chparam -set CKPCE 3 -set CWIDTH 20 -set IWIDTH 16 -set F_CHECK 2 butterfly
 
prep -top butterfly
 
[files]
abs_mpy.v
../../rtl/convround.v
../../rtl/bimpy.v
../../rtl/longbimpy.v
../../rtl/convround.v
../../rtl/butterfly.v
/dblclockfft/trunk/bench/formal/fftstage.sby
0,0 → 1,25
[tasks]
s2
s3
s4
s5
s6
 
[options]
mode prove
depth 12
 
[engines]
smtbmc
 
[script]
read -formal fftstage.v
s2: chparam -set LGSPAN 2
s3: chparam -set LGSPAN 3
s4: chparam -set LGSPAN 4
s5: chparam -set LGSPAN 5
s6: chparam -set LGSPAN 6
prep -top fftstage
 
[files]
../../rtl/fftstage.v
/dblclockfft/trunk/bench/formal/longbimpy.sby
0,0 → 1,15
[options]
mode prove
depth 20
 
[engines]
smtbmc
 
[script]
read -formal -DLONGBIMPY longbimpy.v
read -formal -DLONGBIMPY bimpy.v
prep -top longbimpy
 
[files]
../../rtl/longbimpy.v
../../rtl/bimpy.v
/dblclockfft/trunk/bench/formal/windowfn.sby
0,0 → 1,19
[tasks]
cover
proof
 
[options]
proof: mode prove
proof: depth 10
cover: mode cover
cover: depth 60
 
[engines]
smtbmc
 
[script]
read_verilog -formal -DWINDOWFN windowfn.v
prep -top windowfn
 
[files]
../../rtl/windowfn.v
/dblclockfft/trunk/bench/formal
dblclockfft/trunk/bench/formal Property changes : Added: svn:ignore ## -0,0 +1 ## +fftstage_s2

powered by: WebSVN 2.1.0

© copyright 1999-2024 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.