| 1 |
40 |
dgisselq |
################################################################################
|
| 2 |
|
|
##
|
| 3 |
|
|
## Filename: bench/formal/Makefile
|
| 4 |
|
|
##
|
| 5 |
|
|
## Project: A General Purpose Pipelined FFT Implementation
|
| 6 |
|
|
##
|
| 7 |
|
|
## Purpose: Runs all of the SymbiYosys enabled formal proofs. Requires
|
| 8 |
|
|
## the formal code within the various modules to be enabled.
|
| 9 |
|
|
##
|
| 10 |
|
|
## Creator: Dan Gisselquist, Ph.D.
|
| 11 |
|
|
## Gisselquist Technology, LLC
|
| 12 |
|
|
##
|
| 13 |
|
|
################################################################################
|
| 14 |
|
|
##
|
| 15 |
|
|
## Copyright (C) 2018, Gisselquist Technology, LLC
|
| 16 |
|
|
##
|
| 17 |
|
|
## This file is part of the general purpose pipelined FFT project.
|
| 18 |
|
|
##
|
| 19 |
|
|
## The pipelined FFT project is free software (firmware): you can redistribute
|
| 20 |
|
|
## it and/or modify it under the terms of the GNU Lesser General Public License
|
| 21 |
|
|
## as published by the Free Software Foundation, either version 3 of the
|
| 22 |
|
|
## License, or (at your option) any later version.
|
| 23 |
|
|
##
|
| 24 |
|
|
## The pipelined FFT project is distributed in the hope that it will be useful,
|
| 25 |
|
|
## but WITHOUT ANY WARRANTY; without even the implied warranty of
|
| 26 |
|
|
## MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser
|
| 27 |
|
|
## General Public License for more details.
|
| 28 |
|
|
##
|
| 29 |
|
|
## You should have received a copy of the GNU Lesser General Public License
|
| 30 |
|
|
## along with this program. (It's in the $(ROOT)/doc directory. Run make
|
| 31 |
|
|
## with no target there if the PDF file isn't present.) If not, see
|
| 32 |
|
|
## for a copy.
|
| 33 |
|
|
##
|
| 34 |
|
|
## License: LGPL, v3, as defined and found on www.gnu.org,
|
| 35 |
|
|
## http://www.gnu.org/licenses/lgpl.html
|
| 36 |
|
|
##
|
| 37 |
|
|
##
|
| 38 |
|
|
################################################################################
|
| 39 |
|
|
##
|
| 40 |
|
|
##
|
| 41 |
|
|
TARGETS := bimpy longbimpy fftstage hwbfly butterfly qtrstage laststage bitreverse
|
| 42 |
|
|
.PHONY: $(TARGETS)
|
| 43 |
|
|
all: bimpy longbimpy hwbfly fftstage qtrstage laststage bitreverse # butterfly
|
| 44 |
|
|
|
| 45 |
|
|
bimpy:
|
| 46 |
|
|
sby -f bimpy.sby
|
| 47 |
|
|
|
| 48 |
|
|
longbimpy:
|
| 49 |
|
|
sby -f longbimpy.sby
|
| 50 |
|
|
|
| 51 |
|
|
fftstage:
|
| 52 |
|
|
sby -f fftstage.sby
|
| 53 |
|
|
|
| 54 |
|
|
hwbfly:
|
| 55 |
|
|
sby -f hwbfly.sby
|
| 56 |
|
|
|
| 57 |
|
|
butterfly:
|
| 58 |
|
|
sby -f butterfly.sby
|
| 59 |
|
|
|
| 60 |
|
|
qtrstage:
|
| 61 |
|
|
sby -f qtrstage.sby
|
| 62 |
|
|
|
| 63 |
|
|
laststage:
|
| 64 |
|
|
sby -f laststage.sby
|
| 65 |
|
|
|
| 66 |
|
|
bitreverse:
|
| 67 |
|
|
sby -f bitreverse.sby
|
| 68 |
|
|
|
| 69 |
|
|
windowfn:
|
| 70 |
|
|
sby -f windowfn.sby
|
| 71 |
|
|
|
| 72 |
|
|
clean:
|
| 73 |
|
|
rm -rf bimpy/ longbimpy/
|
| 74 |
|
|
rm -rf bitreverse/
|
| 75 |
|
|
rm -rf butterfly_ck1/
|
| 76 |
|
|
rm -rf butterfly_ck2_r0/
|
| 77 |
|
|
rm -rf butterfly_ck2_r1/
|
| 78 |
|
|
rm -rf butterfly_ck3_r0/
|
| 79 |
|
|
rm -rf butterfly_ck3_r1/
|
| 80 |
|
|
rm -rf butterfly_ck3_r2/
|
| 81 |
|
|
rm -rf fftstage_s2/ fftstage_s3/ fftstage_s4/ fftstage_s5/ fftstage_s6/
|
| 82 |
|
|
rm -rf hwbfly_one/ hwbfly_two/ hwbfly_three/
|
| 83 |
|
|
rm -rf laststage/ qtrstage/
|
| 84 |
|
|
rm -rf windowfn_cover/ windowfn_proof/
|
