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

Subversion Repositories zipcpu

Compare Revisions

  • This comparison shows the changes necessary to convert path 
    /zipcpu/trunk/bench
    from Rev 204 to Rev 209
    ↔ Reverse comparison
  •

Rev 204 → Rev 209

/asm/Makefile
1,69 → 1,72
################################################################################
#
# Filename: Makefile
#
# Project: Zip CPU -- a small, lightweight, RISC CPU soft core
#
# Purpose: To direct and simplify the build of a variety of simple assembly
# language test programs which will use one (or both) of the
# ZipCPU simulators.
#
# Targets include:
#
# hellosim
# Using the SIM instruction, prints Hello World to the screen.
#
# simuart
# Same as hellosim, but without using the SIM instruction. This
# *should* be able to run successfully on a verilated or
# synthesized hardware, although I hvae yet to test it there.
#
# simtest
# A set of simple tests designed to demonstrate if the simulator
# works or not.
#
# clean
# Removes the object file directory and any executables that have
# been created.
#
# None of the files/targets below have any dependencies, or if they did,
# GCC can't determine them, so thus there is no make depends step.
#
# To actually run one of these programs, list the program on the command
# line with the ZipCPU simulator, zsim.
#
#
#
# Creator: Dan Gisselquist, Ph.D.
# Gisselquist Technology, LLC
#
##
## Filename: Makefile
##
## Project: Zip CPU -- a small, lightweight, RISC CPU soft core
##
## Purpose: To direct and simplify the build of a variety of simple assembly
## language test programs which will use one (or both) of the
## ZipCPU simulators.
##
## Targets include:
##
## hellosim
## Using the SIM instruction, prints Hello World to the screen.
##
## simuart
## Same as hellosim, but without using the SIM instruction. This
## *should* be able to run successfully on a verilated or
## synthesized hardware, although I hvae yet to test it there.
##
## simtest
## A set of simple tests designed to demonstrate if the simulator
## works or not.
##
## clean
## Removes the object file directory and any executables that have
## been created.
##
## None of the files/targets below have any dependencies, or if they did,
## GCC can't determine them, so thus there is no make depends step.
##
## To actually run one of these programs, list the program on the command
## line with the ZipCPU simulator, zsim.
##
##
##
## Creator: Dan Gisselquist, Ph.D.
## Gisselquist Technology, LLC
##
################################################################################
#
# Copyright (C) 2017, 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
#
#
##
## Copyright (C) 2017, 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
##
##
################################################################################
#
##
##
.PHONY: all
all: $(OBJDIR)/ hellosim simtest simuart cmptest
all:
PROGRAMS := hellosim simuart simtest cmptest
all: $(PROGRAMS)
 
CC := zip-gcc
CPP := zip-cpp
74,12 → 77,14
CFLAGS := -O3
LIBD := ../../sw/install/cross-tools/zip/lib
LIBS := -L$(LIBD) -lzipbasic
LDSCRIPT:= ../zipsim.ld
LDSCRIPT:= ./simscript.ld
 
$(OBJDIR)/%.o: %.c $(OBJDIR)/
$(OBJDIR)/%.o: %.c
$(mk-objdir)
$(CC) $(CFLAGS) -c $< -o $@
 
$(OBJDIR)/%.o: %.s $(OBJDIR)/
$(OBJDIR)/%.o: %.s
$(mk-objdir)
$(AS) $< -o $@
 
%.txt: %
113,7 → 118,8
# needs to be run through the C pre-processor before it can go through the
# assembler. Hence the build is a tocuh trickier, but still simple enough.
#
$(OBJDIR)/simtest.o: simtest.s $(OBJDIR)/
$(OBJDIR)/simtest.o: simtest.s
$(mk-objdir)
$(CPP) $< > $(OBJDIR)/simtest.s
$(AS) $(OBJDIR)/simtest.s -o $@
 
124,10 → 130,15
$(LD) -T $(LDSCRIPT) -Map=map.txt $< -o $@
 
 
$(OBJDIR)/:
define mk-objdir
@bash -c "if [[ ! -e $(OBJDIR) ]]; then mkdir -p $(OBJDIR)/; fi"
endef
 
tags: $(wildcard *.c) $(wildcard *.h) $(wildcard *.cpp)
@echo "Generating tags"
@ctags $(wildcard *.c) $(wildcard *.h)
 
.PHONY: clean
clean:
rm -rf $(OBJDIR)/
rm -rf hellosim simuart simtest
rm -rf $(PROGRAMS)
/asm/zipdhry.S
7,6 → 7,19
; Purpose: Zip assembly file for running the Dhrystone benchmark in the
; Zip CPU.
;
; ****************************
;
; This file is long since out of date. It is kept around for historical
; reasons only. In many ways, this file never truly accomplished the
; Dhrystone test, since it is an assembly file (not compiled), and since
; it uses internally and locally optimized library versions.
;
; Another version of Dhrystone exists for the ZipCPU, in C, which properly
; executes the benchmark.
;
; ****************************
;
;
; To calculate a DMIPS value, take the value of R0 upon completion. This
; is the number of clock ticks used from start to finish (i.e., from
; entrance into user mode to the return to supervisor mode). Let
/cpp/Makefile
1,46 → 1,47
################################################################################
#
# Filename: Makefile
#
# Project: Zip CPU -- a small, lightweight, RISC CPU soft core
#
# Purpose: To direct and simplify the build of a variety of simple test
# programs which will use one (or both) of the ZipCPU simulators.
#
# Targets include:
#
# helloworld
#
#
#
# Creator: Dan Gisselquist, Ph.D.
# Gisselquist Technology, LLC
#
##
## Filename: Makefile
##
## Project: Zip CPU -- a small, lightweight, RISC CPU soft core
##
## Purpose: To direct and simplify the build of a variety of simple test
## programs which will use one (or both) of the ZipCPU simulators.
##
## Targets include:
##
## helloworld
##
##
##
## Creator: Dan Gisselquist, Ph.D.
## Gisselquist Technology, LLC
##
################################################################################
#
# Copyright (C) 2017, 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
#
#
##
## Copyright (C) 2017-2019, 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
##
##
################################################################################
#
##
##
.PHONY: all
all: helloworld
 
/cpp/README.md
0,0 → 1,6
At one time, this was the directory containing the ZipCPU bench simulation.
 
That simulation has now moved to the [sim/verilator](sim/verilator) directory.
 
Therefore, I expect to remove this directory in the future--it's not really
serving a purpose anymore.
/cpp/helloworld.c
9,27 → 9,11
// run with no O/S.
//
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2016, Gisselquist Technology, LLC
// Gisselquist Technology asserts no ownership rights over this particular
// hello world program.
//
// 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.
//
// License: GPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/gpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
/formal/.gitignore
0,0 → 1,27
*.check
*.smt2
*.yslog
*.blif
zipcpu
old
zipcpu_*/
dcache_*/
div
memops_*/
idecode_*/
pipemem_*/
wbdmac
zipcounter
ziptimer
zipjiffies
icontrol
wbwatchdog
busdelay
cpuops
dblfetch
pfcache_prf
pfcache_cvr
prefetch
wbdblpriarb
wbpriarbiter
zipmmu
/formal/Makefile
0,0 → 1,282
################################################################################
##
## Filename: Makefile
##
## Project: Zip CPU -- a small, lightweight, RISC CPU soft core
##
## Purpose: To direct the formal verification of particular components of
## the ZipCPU.
##
## Targets: The default target, all, tests all of the components within
## this module.
##
## Creator: Dan Gisselquist, Ph.D.
## Gisselquist Technology, LLC
##
################################################################################
##
## Copyright (C) 2017-2019, 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
##
##
################################################################################
##
##
TESTS := prefetch dblfetch pfcache memops pipemem idecode div
TESTS += zipmmu ziptimer zipcounter zipjiffies wbwatchdog zipmmu icontrol wbdmac
TESTS += busdelay wbpriarbiter wbdblpriarb cpuops cpu dcache zipcpu
.PHONY: $(TESTS)
all: $(TESTS)
RTL := ../../rtl
 
SMTBMC := yosys-smtbmc
# SOLVER := -s z3
SOLVER := -s yices
# SOLVER := -s boolector
BMCARGS := --presat $(SOLVER)
INDARGS := $(SOLVER) -i
 
PFONE := prefetch
PFTWO := dblfetch
PFCACHE:= pfcache
WBDLY := busdelay
PRIARB := wbpriarbiter
DBL := wbdblpriarb
PIPE := pipemem
MEM := memops
MMU := zipmmu
TMR := ziptimer
CNT := zipcounter
JIF := zipjiffies
WDG := wbwatchdog
INT := icontrol
DCD := idecode
DMA := wbdmac
ALU := cpuops
DIV := div
CPU := zipcpu
DCACHE := dcache
.PHONY: cpu
cpu: zipcpu
 
MASTER := $(RTL)/ex/fwb_master.v
SLAVE := $(RTL)/ex/fwb_slave.v
 
.PHONY: $(PFONE)
$(PFONE) : $(PFONE)/PASS
$(PFONE)/PASS: $(PFONE).sby $(RTL)/core/$(PFONE).v $(MASTER)
sby -f $(PFONE).sby
 
.PHONY: $(PFTWO)
$(PFTWO) : $(PFTWO)/PASS
$(PFTWO)/PASS: $(PFTWO).sby $(RTL)/core/$(PFTWO).v $(MASTER)
sby -f $(PFTWO).sby
 
 
.PHONY: $(PFCACHE)
$(PFCACHE): $(PFCACHE)_prf/PASS $(PFCACHE)_cvr/PASS
$(PFCACHE)_prf/PASS: $(PFCACHE).sby $(RTL)/core/$(PFCACHE).v $(MASTER)
sby -f $(PFCACHE).sby prf
$(PFCACHE)_cvr/PASS: $(PFCACHE).sby $(RTL)/core/$(PFCACHE).v $(MASTER)
sby -f $(PFCACHE).sby cvr
 
.PHONY: $(WBDLY)
$(WBDLY): $(WBDLY)/PASS
$(WBDLY)/PASS: $(WBDLY).sby $(RTL)/ex/$(WBDLY).v $(MASTER) $(SLAVE)
sby -f $(WBDLY).sby
 
.PHONY: $(PRIARB)
$(PRIARB): $(PRIARB)/PASS
$(PRIARB)/PASS: $(PRIARB).sby $(RTL)/ex/$(PRIARB).v $(MASTER) $(SLAVE)
sby -f $(PRIARB).sby
 
.PHONY: $(DBL)
$(DBL): $(DBL)/PASS
$(DBL)/PASS: $(DBL).sby $(RTL)/ex/$(DBL).v $(MASTER) $(SLAVE) $(DBL).ys
sby -f $(DBL).sby
 
.PHONY: $(MEM)
$(MEM): $(MEM)_cover/PASS $(MEM)_proof/PASS
$(MEM)_proof/PASS: $(MEM).sby $(RTL)/core/$(MEM).v $(MASTER)
sby -f $(MEM).sby proof
$(MEM)_cover/PASS: $(MEM).sby $(RTL)/core/$(MEM).v $(MASTER)
sby -f $(MEM).sby cover
 
.PHONY: $(PIPE)
$(PIPE): $(PIPE)_lcl_aligned_lock/PASS
$(PIPE): $(PIPE)_lcl_aligned_nolock/PASS
$(PIPE): $(PIPE)_lcl_noaligned_lock/PASS
$(PIPE): $(PIPE)_lcl_noaligned_nolock/PASS
$(PIPE): $(PIPE)_nolcl_aligned_lock/PASS
$(PIPE): $(PIPE)_nolcl_aligned_nolock/PASS
$(PIPE): $(PIPE)_nolcl_noaligned_lock/PASS
$(PIPE): $(PIPE)_nolcl_noaligned_nolock/PASS
$(PIPE)_lcl_aligned_lock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
sby -f $(PIPE).sby lcl_aligned_lock
$(PIPE)_lcl_aligned_nolock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
sby -f $(PIPE).sby lcl_aligned_nolock
$(PIPE)_lcl_noaligned_lock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
sby -f $(PIPE).sby lcl_noaligned_lock
$(PIPE)_lcl_noaligned_nolock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
sby -f $(PIPE).sby lcl_noaligned_nolock
$(PIPE)_nolcl_aligned_lock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
sby -f $(PIPE).sby nolcl_aligned_lock
$(PIPE)_nolcl_aligned_nolock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
sby -f $(PIPE).sby nolcl_aligned_nolock
$(PIPE)_nolcl_noaligned_lock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
sby -f $(PIPE).sby nolcl_noaligned_lock
$(PIPE)_nolcl_noaligned_nolock/PASS: $(PIPE).sby $(RTL)/core/$(PIPE).v $(MASTER)
sby -f $(PIPE).sby nolcl_noaligned_nolock
 
.PHONY: $(MMU)
$(MMU): $(MMU)/PASS
$(MMU)/PASS: $(MMU).sby $(RTL)/peripherals/$(MMU).v $(MASTER) $(SLAVE)
sby -f $(MMU).sby
 
.PHONY: $(TMR)
$(TMR): $(TMR)/PASS
$(TMR)/PASS: $(TMR).sby $(RTL)/peripherals/$(TMR).v $(SLAVE) $(TMR).ys
sby -f $(TMR).sby
 
.PHONY: $(CNT)
$(CNT): $(CNT)/PASS
$(CNT)/PASS: $(CNT).sby $(RTL)/peripherals/$(CNT).v $(SLAVE)
sby -f $(CNT).sby
 
.PHONY: $(JIF)
$(JIF): $(JIF)/PASS
$(JIF)/PASS: $(JIF).sby $(RTL)/peripherals/$(JIF).v $(SLAVE)
sby -f $(JIF).sby
 
.PHONY: $(WDG)
$(WDG): $(WDG)/PASS
$(WDG)/PASS: $(WDG).sby $(RTL)/peripherals/$(WDG).v $(SLAVE)
sby -f $(WDG).sby
 
.PHONY: $(INT)
$(INT): $(INT)/PASS
$(INT)/PASS: $(INT).sby $(RTL)/peripherals/$(INT).v $(SLAVE)
sby -f $(INT).sby
 
.PHONY: $(DCD)
$(DCD): $(DCD)_pipe_div_mpy_cis_opipe/PASS
$(DCD): $(DCD)_pipe_div_mpy_cis_nopipe/PASS
$(DCD): $(DCD)_pipe_div_mpy_nocis_pipe/PASS
$(DCD): $(DCD)_pipe_div_mpy_nocis_nopipe/PASS
$(DCD): $(DCD)_pipe_div_nompy_nocis_nopipe/PASS
$(DCD): $(DCD)_pipe_nodiv_nompy_nocis_nopipe/PASS
$(DCD): $(DCD)_nopipe_nodiv_nompy_nocis_nopipe/PASS
 
$(DCD)_pipe_div_mpy_cis_opipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
sby -f $(DCD).sby pipe_div_mpy_cis_opipe
$(DCD)_pipe_div_mpy_cis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
sby -f $(DCD).sby pipe_div_mpy_cis_nopipe
$(DCD)_pipe_div_mpy_nocis_pipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
sby -f $(DCD).sby pipe_div_mpy_nocis_pipe
$(DCD)_pipe_div_mpy_nocis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
sby -f $(DCD).sby pipe_div_mpy_nocis_nopipe
$(DCD)_pipe_div_nompy_nocis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
sby -f $(DCD).sby pipe_div_nompy_nocis_nopipe
$(DCD)_pipe_nodiv_nompy_nocis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
sby -f $(DCD).sby pipe_nodiv_nompy_nocis_nopipe
$(DCD)_nopipe_nodiv_nompy_nocis_nopipe/PASS: $(RTL)/core/$(DCD).v $(DCD).sby f_idecode.v
sby -f $(DCD).sby nopipe_nodiv_nompy_nocis_nopipe
 
 
.PHONY: $(DMA)
$(DMA): $(DMA)/PASS
$(DMA)/PASS: $(RTL)/peripherals/$(DMA).v $(MASTER) $(SLAVE) $(DMA).sby
sby -f $(DMA).sby
 
.PHONY: $(ALU)
$(ALU): $(ALU)/PASS
$(ALU)/PASS: $(ALU).sby $(RTL)/core/$(ALU).v abs_mpy.v
sby -f $(ALU).sby
 
DCACHE_FILES := $(DCACHE).sby $(RTL)/core/dcache.v $(MASTER) $(RTL)/core/iscachable.v
 
.PHONY: $(DCACHE)
$(DCACHE) : $(DCACHE)_full/PASS $(DCACHE)_full_single/PASS $(DCACHE)_bare/PASS
$(DCACHE) : $(DCACHE)_nolock_nolocal/PASS $(DCACHE)_nolock_system/PASS
$(DCACHE) : $(DCACHE)_piped/PASS $(DCACHE)_cover/PASS $(DCACHE)_cover_pipe/PASS
$(DCACHE)_full/PASS: $(DCACHE_FILES)
sby -f $(DCACHE).sby full
$(DCACHE)_full_single/PASS: $(DCACHE_FILES)
sby -f $(DCACHE).sby full_single
 
$(DCACHE)_bare/PASS: $(DCACHE_FILES)
sby -f $(DCACHE).sby bare
 
$(DCACHE)_nolock_nolocal/PASS: $(DCACHE_FILES)
sby -f $(DCACHE).sby nolock_nolocal
 
$(DCACHE)_nolock_system/PASS: $(DCACHE_FILES)
sby -f $(DCACHE).sby nolock_system
 
$(DCACHE)_piped/PASS: $(DCACHE_FILES)
sby -f $(DCACHE).sby piped
 
$(DCACHE)_cover/PASS: $(DCACHE_FILES)
sby -f $(DCACHE).sby cover
 
$(DCACHE)_cover_pipe/PASS: $(DCACHE_FILES)
sby -f $(DCACHE).sby cover_pipe
 
.PHONY: $(DIV)
$(DIV) : $(DIV)/PASS
$(DIV)/PASS: $(DIV).sby $(RTL)/core/div.v
sby -f $(DIV).sby
 
.PHONY: $(CPU)
$(CPU): $(CPU)_dcache/PASS $(CPU)_piped/PASS
$(CPU): $(CPU)_nopipe/PASS $(CPU)_lowlogic/PASS $(CPU)_ice40/PASS
CPUDEPS:= $(RTL)/core/$(CPU).v $(RTL)/core/cpuops.v $(RTL)/core/idecode.v \
$(RTL)/core/pipemem.v $(RTL)/core/memops.v \
$(RTL)/ex/wbdblpriarb.v $(RTL)/ex/fwb_counter.v $(RTL)/cpudefs.v \
f_idecode.v abs_div.v abs_prefetch.v abs_mpy.v $(MASTER) $(SLAVE) \
$(CPU).sby
$(CPU)_dcache/PASS: $(CPUDEPS) $(RTL)/core/dcache.v $(RTL)/core/iscachable.v
sby -f $(CPU).sby dcache
 
$(CPU)_piped/PASS: $(CPUDEPS)
sby -f $(CPU).sby piped
 
$(CPU)_nopipe/PASS: $(CPUDEPS)
sby -f $(CPU).sby nopipe
 
$(CPU)_lowlogic/PASS: $(CPUDEPS)
sby -f $(CPU).sby lowlogic
 
$(CPU)_ice40/PASS: $(CPUDEPS)
sby -f $(CPU).sby ice40
 
.PHONY: clean
clean:
rm -rf $(PFONE)*/ $(PFTWO)*/ $(PFCACHE)*/
rm -f $(WBDLY).smt2 $(WBDLY)*.vcd $(WBDLY).yslog
rm -f $(PRIARB).smt2 $(PRIARB)*.vcd $(PRIARB).yslog
rm -f $(DBL).smt2 $(DBL)*.vcd $(DBL).yslog
rm -rf $(MEM)*/ $(PIPE)*/ $(MMU)*/
rm -rf $(TMR)*/ $(CNT)*/ $(JIF)*/
rm -rf $(WDG)*/ $(INT)*/ $(DCD)_*/
rm -rf $(DMA)*/ $(ALU)*/ $(DIV)*/
rm -rf $(DCACHE)_*/
rm -rf $(CPU)_*/
rm -f *.check
/formal/abs_div.v
0,0 → 1,217
////////////////////////////////////////////////////////////////////////////////
//
// Filename: abs_div.v
//
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
//
// Purpose: The original divide module provides an Integer divide
// capability to the Zip CPU. This module is an abstract
// divide module. It *might* produce a valid integer divide, either signed
// or unsigned, result. It might instead do somethin else. It is designed
// to be easier for the formal tools to work with.
//
// Steps:
// i_reset The DIVide unit starts in idle. It can also be placed into an
// idle by asserting the reset input.
//
// i_wr When i_reset is asserted, a divide begins. On the next clock:
//
// o_busy is set high so everyone else knows we are at work and they can
// wait for us to complete.
//
// pre_sign is set to true if we need to do a signed divide. In this
// case, we take a clock cycle to turn the divide into an unsigned
// divide.
//
// o_quotient, a place to store our result, is initialized to all zeros.
//
// r_dividend is set to the numerator
//
// r_divisor is set to 2^31 * the denominator (shift left by 31, or add
// 31 zeros to the right of the number.
//
// pre_sign When true (clock cycle after i_wr), a clock cycle is used
// to take the absolute value of the various arguments (r_dividend
// and r_divisor), and to calculate what sign the output result
// should be.
//
//
// At this point, the divide is has started. The divide works by walking
// through every shift of the
//
// DIVIDEND over the
// DIVISOR
//
// If the DIVISOR is bigger than the dividend, the divisor is shifted
// right, and nothing is done to the output quotient.
//
// DIVIDEND
// DIVISOR
//
// This repeats, until DIVISOR is less than or equal to the divident, as in
//
// DIVIDEND
// DIVISOR
//
// At this point, if the DIVISOR is less than the dividend, the
// divisor is subtracted from the dividend, and the DIVISOR is again
// shifted to the right. Further, a '1' bit gets set in the output
// quotient.
//
// Once we've done this for 32 clocks, we've accumulated our answer into
// the output quotient, and we can proceed to the next step. If the
// result will be signed, the next step negates the quotient, otherwise
// it returns the result.
//
// On the clock when we are done, o_busy is set to false, and o_valid set
// to true. (It is a violation of the ZipCPU internal protocol for both
// busy and valid to ever be true on the same clock. It is also a
// violation for busy to be false with valid true thereafter.)
//
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2019, 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 abs_div(i_clk, i_reset, i_wr, i_signed, i_numerator, i_denominator,
o_busy, o_valid, o_err, o_quotient, o_flags);
parameter BW=32, LGBW = 5;
parameter [4:0] MAXDELAY = 3;
input wire i_clk, i_reset;
// Input parameters
input wire i_wr, i_signed;
input wire [(BW-1):0] i_numerator, i_denominator;
// Output parameters
output wire o_busy;
output reg o_valid, o_err;
output reg [(BW-1):0] o_quotient;
output wire [3:0] o_flags;
 
(* anyseq *) reg any_err;
(* anyseq *) reg [(BW-1):0] any_quotient;
(* anyseq *) reg [5:0] wait_time;
 
always @(*)
o_err = any_err;
always @(*)
o_quotient = any_quotient;
 
reg [5:0] r_busy_counter;
 
always @(*)
assume(wait_time > 5'h1);
 
always @(*)
assume((MAXDELAY == 0)||(wait_time < MAXDELAY));
 
initial r_busy_counter = 0;
always @(posedge i_clk)
if (i_reset)
r_busy_counter <= 0;
else if ((i_wr)&&(!o_busy))
r_busy_counter <= wait_time;
else if (r_busy_counter > 0)
r_busy_counter <= r_busy_counter - 1'b1;
 
always @(*)
assert((MAXDELAY == 0)||(r_busy_counter < MAXDELAY));
 
assign o_busy = (r_busy_counter != 0);
 
initial o_valid = 1'b0;
always @(posedge i_clk)
if (i_reset)
o_valid <= 1'b0;
else
o_valid <= (r_busy_counter == 1);
 
(* anyseq *) reg [3:0] any_flags;
 
assign o_flags = (o_valid) ?
{ 1'b0, o_quotient[31], any_flags[1],
(o_quotient == 0) } : any_flags;
 
`ifdef FORMAL
reg f_past_valid;
initial f_past_valid = 0;
always @(posedge i_clk)
f_past_valid <= 1'b1;
always @(posedge i_clk)
if (!f_past_valid)
assert((!o_busy)&&(!o_valid));
 
`define ASSUME assert
 
initial `ASSUME(i_reset);
always @(*)
if (!f_past_valid)
`ASSUME(i_reset);
 
always @(posedge i_clk)
if ((!f_past_valid)||($past(i_reset)))
`ASSUME(!i_wr);
 
always @(*)
if (o_busy)
`ASSUME(!i_wr);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(o_busy))&&(!o_busy))
assume(o_valid);
 
always @(*)
if (o_err)
assume(o_valid);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wr)))
assert(o_busy);
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(o_valid)))
assume(!o_valid);
 
always @(*)
if ((o_valid)&&(!o_err))
assume(o_flags[3] == ((o_quotient == 0)? 1'b1:1'b0));
 
always @(*)
if ((o_valid)&&(!o_err))
assume(o_flags[1] == o_quotient[BW-1]);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(o_busy))&&(!$past(i_wr)))
assume(!o_busy);
 
always @(posedge i_clk)
assume((!o_busy)||(!o_valid));
 
`endif
endmodule
/formal/abs_mpy.v
0,0 → 1,129
////////////////////////////////////////////////////////////////////////////////
//
// Filename: abs_mpy.v
//
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
//
// Purpose: This code has been modified from the mpyop.v file so as to
// abstract the multiply that formal methods struggle so hard to
// deal with. It also simplifies the interface so that (if enabled)
// the multiply will return in 1-6 clocks, rather than the specified
// number for the given architecture.
//
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2019, 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 abs_mpy(i_clk,i_reset, i_stb, i_op, i_a, i_b, o_valid, o_busy, o_result, o_hi);
// The following parameter selects which multiply algorithm we use.
// Timing performance is strictly dependent upon it.
parameter IMPLEMENT_MPY = 1;
parameter MAXDELAY = 3;
input wire i_clk, i_reset, i_stb;
input wire [1:0] i_op; // 2'b00=MPY, 2'b10=MPYUHI, 2'b11=MPYSHI
input wire [31:0] i_a, i_b;
output reg o_valid; // True if we'll be valid on the next clock;
output wire o_busy; // The multiply is busy if true
output wire [63:0] o_result; // Where we dump the multiply result
output reg o_hi; // Return the high half of the multiply
 
`define ASSERT assert
// i_stb instead of this_is_a_multiply_op
// o_result
// o_busy
// o_done
generate
if (IMPLEMENT_MPY == 0)
begin // No multiply support.
 
assign o_result = 64'h00;
assign o_busy = 1'b0;
always @(*)
o_valid = i_stb;
always @(*) o_hi = 1'b0; // Not needed
 
end else begin // Our single clock option (no extra clocks)
 
(* anyseq *) reg [2:0] next_delay_to_valid;
(* anyseq *) reg [63:0] any_result;
 
assign o_result = any_result;
 
reg [2:0] delay_to_valid;
reg r_busy;
 
always @(*)
assume((MAXDELAY == 0)
||(next_delay_to_valid < MAXDELAY));
 
// always @(*)
// if (IMPLEMENT_MPY == 1)
// assume(next_delay_to_valid == 0);
always @(*)
if (IMPLEMENT_MPY>0)
assume(next_delay_to_valid == IMPLEMENT_MPY-1);
 
initial delay_to_valid = 3'h0;
always @(posedge i_clk)
if (i_reset)
delay_to_valid <= 0;
else if ((i_stb)&&(next_delay_to_valid != 0))
delay_to_valid <= next_delay_to_valid;
else if (delay_to_valid > 0)
delay_to_valid <= delay_to_valid - 1'b1;
 
initial r_busy = 1'b0;
always @(posedge i_clk)
if (i_reset)
r_busy <= 1'b0;
else if (i_stb)
r_busy <= (next_delay_to_valid != 0);
else if (r_busy)
r_busy <= (delay_to_valid != 3'h1);
 
initial o_valid = 0;
always @(posedge i_clk)
if (i_reset)
o_valid <= 1'b0;
else if ((i_stb)&&(next_delay_to_valid == 0))
o_valid <= 1'b1;
else
o_valid <= (o_busy)&&(delay_to_valid == 3'h1);
 
always @(posedge i_clk)
if (i_stb)
o_hi <= i_op[1];
 
assign o_busy = r_busy;
end
endgenerate // All possible multiply results have been determined
 
endmodule
/formal/abs_prefetch.v
0,0 → 1,268
////////////////////////////////////////////////////////////////////////////////
//
// Filename: abs_prefetch.v
//
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
//
// Purpose: Rather than feed our CPU with actual valid instructions returned
// from memory, this is an abstract prefetch. It's not even a
// perfect or complete abstract prefetch at that--it doesn't actually
// access memory. However, it will maintain the abstract interface with
// the CPU.s
//
// In other words, this abs_prefetch may produce the exact same results a
// true prefetch would have produced--whether it be prefetch.v, dblfetch.v,
// or even pfcache.v. On the other hand, it might not. If the CPU can
// pass either way, then it can most certainly pass with a true prefetch.
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2019, 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 abs_prefetch(i_clk, i_reset, i_new_pc, i_clear_cache,
// i_early_branch, i_from_addr,
i_stall_n, i_pc, o_insn, o_pc, o_valid,
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
i_wb_ack, i_wb_stall, i_wb_err, i_wb_data,
o_illegal);
parameter ADDRESS_WIDTH = 30;
localparam BUSW = 32; // Number of data lines on the bus
localparam AW=ADDRESS_WIDTH; // Shorthand for ADDRESS_WIDTH
//
input wire i_clk, i_reset;
//
// The interface with the rest of the CPU
input wire i_new_pc;
input wire i_clear_cache;
input wire i_stall_n;
input wire [(AW+1):0] i_pc;
output wire [(BUSW-1):0] o_insn;
output wire [(AW+1):0] o_pc;
output wire o_valid;
//
// The wishbone bus interface
output wire o_wb_cyc, o_wb_stb;
output wire o_wb_we;
output wire [(AW-1):0] o_wb_addr;
output wire [(BUSW-1):0] o_wb_data;
//
input wire i_wb_ack, i_wb_stall, i_wb_err;
input wire [(BUSW-1):0] i_wb_data;
//
// o_illegal will be true if this instruction was the result of
// a bus error (This is also part of the CPU interface)
output reg o_illegal;
//
 
// Fixed bus outputs: we read from the bus only, never write.
// Thus the output data is ... irrelevant and don't care. We set it
// to zero just to set it to something.
assign o_wb_cyc = 0;
assign o_wb_stb = 0;
assign o_wb_we = 0;
assign o_wb_addr = 0;
assign o_wb_data = 0;
 
 
reg [(AW-1):0] r_pc;
reg waiting_on_pc;
reg [5:0] wait_for_valid;
 
 
 
always @(posedge i_clk)
if (i_new_pc)
r_pc = i_pc[AW+1:2];
else if ((o_valid)&&(i_stall_n))
r_pc <= r_pc + 1'b1;
 
(* anyconst *) reg [(AW-1):0] any_pc;
assign o_pc = { (o_valid) ? r_pc : any_pc, 2'b00 };
 
 
(* anyseq *) reg any_illegal;
always @(posedge i_clk)
if ((i_reset)||(i_clear_cache)||(i_new_pc)||(waiting_on_pc))
o_illegal <= 1'b0;
else if ((!o_illegal)&&(wait_for_valid == 1'b1))
o_illegal <= any_illegal;
 
(* anyseq *) reg [5:0] wait_time;
always @(*)
assume(wait_time > 0);
 
initial waiting_on_pc <= 1'b1;
always @(posedge i_clk)
if ((i_reset)||(i_clear_cache))
waiting_on_pc <= 1'b1;
else if (i_new_pc)
waiting_on_pc <= 1'b0;
 
always @(posedge i_clk)
if ((i_reset)||(i_clear_cache))
wait_for_valid <= 6'h3f;
else if ((i_new_pc)||(waiting_on_pc))
wait_for_valid <= wait_time;
else if (wait_for_valid > 0)
wait_for_valid <= wait_for_valid - 1'b1;
 
(* anyseq *) reg [(BUSW-1):0] any_insn;
 
assign o_valid = (!waiting_on_pc)&&(wait_for_valid == 0);
assign o_insn = any_insn;
 
`ifdef FORMAL
`define ASSUME assume
`define ASSERT assert
 
// Keep track of a flag telling us whether or not $past()
// will return valid results
reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge i_clk)
f_past_valid = 1'b1;
always @(*)
if (!f_past_valid)
`ASSERT(i_reset);
 
/////////////////////////////////////////////////
//
//
// Assumptions about our inputs
//
//
/////////////////////////////////////////////////
 
//
// Assume we start from a reset condition
initial `ASSERT(i_reset);
 
/////////////////////////////////////////////////
//
//
// Assertions about our outputs
//
//
/////////////////////////////////////////////////
 
/////////////////////////////////////////////////////
//
//
// Assertions about our return responses to the CPU
//
//
/////////////////////////////////////////////////////
 
// Consider it invalid to present the CPU with the same instruction
// twice in a row.
always @(posedge i_clk)
if ((f_past_valid)&&($past(o_valid))&&($past(i_stall_n))&&(o_valid))
assume(o_pc != $past(o_pc));
 
always @(*)
begin
`ASSERT(i_pc[1:0] == 2'b00);
assume(o_pc[1:0] == 2'b00);
end
 
 
//
// Assume we start from a reset condition
initial `ASSUME(i_reset);
 
// Assume that any reset is either accompanied by a new address,
// or a new address immediately follows it.
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
`ASSERT(i_new_pc);
 
//
//
// The bottom two bits of the PC address register are always zero.
// They are there to make examining traces easier, but I expect
// the synthesis tool to remove them.
//
always @(*)
`ASSERT(i_pc[1:0] == 2'b00);
 
// Some things to know from the CPU ... there will always be a
// i_new_pc request following any reset
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
`ASSERT(i_new_pc);
 
// There will also be a i_new_pc request following any request to clear
// the cache.
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_clear_cache)))
`ASSERT(i_new_pc);
 
always @(*)
`ASSUME(i_pc[1:0] == 2'b00);
 
/////////////////////////////////////////////////
//
//
// Assertions about our outputs
//
//
/////////////////////////////////////////////////
 
//
// Assertions about our return responses to the CPU
//
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))
&&(!$past(i_new_pc))&&(!$past(i_clear_cache))
&&($past(o_valid))&&(!$past(i_stall_n)))
begin
assume($stable(o_pc));
assume($stable(o_insn));
assume($stable(o_valid));
assume($stable(o_illegal));
end
 
//
// As with i_pc[1:0], the bottom two bits of the address are unused.
// Let's assert here that they remain zero.
always @(*)
assume(o_pc[1:0] == 2'b00);
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(o_illegal))&&(o_illegal))
assume(o_valid);
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_new_pc)))
assume(!o_valid);
 
`endif // FORMAL
 
endmodule
/formal/busdelay.sby
0,0 → 1,17
[options]
mode prove
depth 25
 
[engines]
smtbmc
 
[script]
read -formal -D BUSDELAY busdelay.v
read -formal -D BUSDELAY fwb_slave.v
read -formal -D BUSDELAY fwb_master.v
prep -top busdelay
 
[files]
../../rtl/ex/busdelay.v
../../rtl/ex/fwb_slave.v
../../rtl/ex/fwb_master.v
/formal/cpuops.sby
0,0 → 1,21
[options]
mode prove
depth 4
 
[engines]
smtbmc
 
[script]
read -formal -D CPUOPS cpuops.v
# read -formal -D CPUOPS mpyop.v
read -formal -D CPUOPS abs_mpy.v
chparam -set IMPLYMENT_MPY 3 cpuops.v
prep -top cpuops
 
[files]
../../rtl/core/cpuops.v
../../rtl/core/mpyop.v
../../rtl/cpudefs.v
abs_mpy.v
 
 
/formal/dblfetch.sby
0,0 → 1,15
[options]
mode prove
depth 8
 
[engines]
smtbmc
 
[script]
read -formal -DDBLFETCH fwb_master.v
read -formal -DDBLFETCH dblfetch.v
prep -top dblfetch
 
[files]
../../rtl/core/dblfetch.v
../../rtl/ex/fwb_master.v
/formal/dcache.gtkw
0,0 → 1,170
[*]
[*] GTKWave Analyzer v3.3.98 (w)1999-2018 BSI
[*] Sat Dec 8 19:23:32 2018
[*]
[dumpfile] "/home/dan/work/rnd/zipcpu/trunk/bench/formal/dcache_piped/engine_0/trace.vcd"
[dumpfile_mtime] "Sat Dec 8 19:20:42 2018"
[dumpfile_size] 53195
[savefile] "/home/dan/work/rnd/zipcpu/trunk/bench/formal/dcache.gtkw"
[timestart] 0
[size] 1918 1021
[pos] -1 -1
*-4.957688 50 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[treeopen] dcache.
[sst_width] 196
[signals_width] 240
[sst_expanded] 1
[sst_vpaned_height] 378
@28
dcache.i_reset
dcache.i_clk
dcache.i_lock
dcache.r_svalid
dcache.r_dvalid
dcache.i_pipe_stb
dcache.o_pipe_stalled
dcache.o_busy
[color] 1
dcache.state[1:0]
dcache.i_op[2:0]
@22
dcache.i_oreg[4:0]
dcache.i_addr[31:0]
dcache.i_data[31:0]
@200
-
@22
dcache.o_wreg[4:0]
dcache.o_data[31:0]
@28
dcache.o_err
dcache.o_valid
@200
-
@28
[color] 3
dcache.o_wb_cyc_gbl
[color] 3
dcache.o_wb_stb_gbl
@200
-
@28
[color] 3
dcache.o_wb_cyc_lcl
[color] 3
dcache.o_wb_stb_lcl
@200
-
@28
[color] 3
dcache.o_wb_we
@22
[color] 3
dcache.o_wb_addr[29:0]
[color] 3
dcache.o_wb_data[31:0]
[color] 3
dcache.o_wb_sel[3:0]
@200
-
@28
[color] 2
dcache.i_wb_stall
[color] 2
dcache.i_wb_ack
@22
[color] 2
dcache.i_wb_data[31:0]
@28
[color] 2
dcache.i_wb_err
@200
-
@22
[color] 3
dcache.c_v[15:0]
@28
[color] 3
dcache.c_wr
@22
[color] 3
dcache.c_wdata[31:0]
@28
dcache.cache_miss_inow
@22
dcache.cached_idata[31:0]
dcache.cached_rdata[31:0]
dcache.f_cache_waddr[29:0]
@200
-
@22
dcache.f_const_tag[28:0]
dcache.f_const_tag_addr[3:0]
dcache.f_const_addr[30:0]
@28
dcache.f_const_buserr
@200
-
@23
dcache.f_ctag_here[28:0]
@22
dcache.f_cmem_here[31:0]
@200
-
@28
dcache.f_this_return
@22
[color] 3
dcache.f_const_data[31:0]
@28
dcache.f_cyc
dcache.f_cachable_r_addr
dcache.f_wb_cachable
dcache.f_cachable_last_tag
dcache.f_past_valid
dcache.f_stb
dcache.f_this_cache_waddr
dcache.f_wb_cachable
dcache.in_cache
@200
-
@28
dcache.last_ack
dcache.last_line_stb
dcache.end_of_line
@200
-
@22
dcache.last_tag[28:0]
@28
dcache.last_tag_valid
@22
dcache.r_ctag[28:0]
@200
-
@22
dcache.f_cmem_here[31:0]
dcache.f_const_data[31:0]
@200
-
@28
dcache.lock_gbl
dcache.lock_lcl
@22
dcache.r_addr[29:0]
@28
dcache.r_cachable
dcache.r_cache_miss
dcache.r_iv
dcache.r_rd
[color] 1
dcache.r_rd_pending
dcache.r_wb_cyc_gbl
dcache.r_wb_cyc_lcl
dcache.stb
dcache.w_cachable
dcache.raw_cachable_address
dcache.wr_cstb
dcache.cyc
[pattern_trace] 1
[pattern_trace] 0
/formal/dcache.sby
0,0 → 1,48
[tasks]
full system lock dualread
full_single system lock
bare nolocal lock dualread
nolock_nolocal nolocal nolock dualread
nolock_system system nolock dualread
piped system lock dualread
cover system lock dualread
cover_pipe system lock dualread cover piped
 
[options]
~cover: mode prove
cover: mode cover
depth 16
full: depth 10
bare: depth 11
nolock_nolocal: depth 11
nolock_system: depth 11
piped: depth 11
cover: depth 24
cover_pipe: depth 45
 
[engines]
# smtbmc yices
smtbmc --nopresat boolector
# abc pdr
# aiger suprove
# aiger avy
 
[script]
read -formal -D DCACHE fwb_master.v
read -formal -D DCACHE iscachable.v
read -formal -D DCACHE dcache.v
piped: chparam -set OPT_PIPE 1 dcache
~piped: chparam -set OPT_PIPE 0 dcache
dualread: chparam -set OPT_DUAL_READ_PORT 1 dcache
~dualread: chparam -set OPT_DUAL_READ_PORT 0 dcache
lock: chparam -set OPT_LOCK 1 dcache
system: chparam -set OPT_LOCAL_BUS 1 dcache
nolock: chparam -set OPT_LOCK 0 dcache
nolocal: chparam -set OPT_LOCAL_BUS 0 dcache
prep -top dcache
 
[files]
../../rtl/core/dcache.v
../../rtl/core/iscachable.v
../../rtl/ex/fwb_master.v
#
/formal/div.gtkw
0,0 → 1,70
[*]
[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
[*] Sat Aug 11 16:11:56 2018
[*]
[dumpfile] "/home/dan/jericho/work/rnd/zipcpu/trunk/bench/formal/div.vcd"
[dumpfile_mtime] "Sat Aug 11 15:44:52 2018"
[dumpfile_size] 3746
[savefile] "/home/dan/jericho/work/rnd/zipcpu/trunk/sim/verilator/div_tb.gtkw"
[timestart] 0
[size] 1698 819
[pos] -1 -1
*-4.333802 30 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 270
[signals_width] 220
[sst_expanded] 1
[sst_vpaned_height] 221
@28
smt_clock
div.i_clk
div.i_reset
@200
-
@28
[color] 2
div.i_wr
[color] 2
div.i_signed
@22
[color] 2
div.i_numerator[31:0]
[color] 2
div.i_denominator[31:0]
@200
-
@28
[color] 3
div.o_busy
[color] 3
div.o_valid
@22
[color] 3
div.o_flags[3:0]
[color] 3
div.o_quotient[31:0]
@28
[color] 3
div.o_err
@200
-
@22
div.r_bit[4:0]
@28
div.pre_sign
div.r_busy
div.r_sign
@29
div.last_bit
@22
div.diff[32:0]
div.r_dividend[62:0]
div.r_divisor[31:0]
@28
div.r_c
div.r_z
div.w_n
div.zero_divisor
@22
div.f_bits_set[32:0]
[pattern_trace] 1
[pattern_trace] 0
/formal/div.sby
0,0 → 1,13
[options]
mode prove
depth 5
 
[engines]
smtbmc
 
[script]
read -formal -DDIV div.v
prep -top div
 
[files]
../../rtl/core/div.v
/formal/f_idecode.v
0,0 → 1,375
////////////////////////////////////////////////////////////////////////////////
//
// Filename: f_idecode.v
//
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
//
// Purpose: This RTL file is meant to shadow the idecode.v file, but yet
// to require no clocks for decoding at all. The purpose is to
// help to verify instructions as they go through the ZipCPU pipeline,
// and so to know what instructions are supposed to do what when.
//
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2018-2019, 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
//
`define CPU_SP_REG 4'hd
`define CPU_CC_REG 4'he
`define CPU_PC_REG 4'hf
//
`define CISBIT 31
`define CISIMMSEL 23
`define IMMSEL 18
//
//
//
module f_idecode(i_instruction, i_phase, i_gie,
o_illegal,
o_dcdR, o_dcdA, o_dcdB, o_I, o_cond, o_wF,
o_op, o_ALU, o_M, o_DV, o_FP, o_break, o_lock,
o_wR, o_rA, o_rB, o_prepipe, o_sim, o_sim_immv
);
parameter ADDRESS_WIDTH=24;
parameter [0:0] OPT_MPY = 1'b1;
parameter [0:0] OPT_EARLY_BRANCHING = 1'b1;
parameter [0:0] OPT_DIVIDE = 1'b1;
parameter [0:0] OPT_FPU = 1'b0;
parameter [0:0] OPT_CIS = 1'b1;
parameter [0:0] OPT_LOCK = 1'b1;
parameter [0:0] OPT_OPIPE = 1'b1;
parameter [0:0] OPT_SIM = 1'b0;
localparam AW = ADDRESS_WIDTH;
//
input wire [31:0] i_instruction;
input wire i_phase, i_gie;
output reg o_illegal;
output wire [6:0] o_dcdR, o_dcdA, o_dcdB;
output wire [31:0] o_I;
output wire [3:0] o_cond;
output wire o_wF;
output wire [3:0] o_op;
output wire o_ALU, o_M, o_DV, o_FP, o_break;
output wire o_lock;
output wire o_wR, o_rA, o_rB;
output wire o_prepipe;
output wire o_sim;
output wire [22:0] o_sim_immv;
 
 
wire [4:0] w_op;
wire w_ldi, w_mov, w_cmptst, w_ldilo, w_ALU, w_brev,
w_noop, w_lock, w_sim, w_break, w_special, w_add,
w_mpy;
wire [4:0] w_dcdR, w_dcdB, w_dcdA;
wire w_dcdR_pc, w_dcdR_cc;
wire w_dcdA_pc, w_dcdA_cc;
wire w_dcdB_pc, w_dcdB_cc;
wire [3:0] w_cond;
wire w_wF, w_mem, w_sto, w_div, w_fpu;
wire w_wR, w_rA, w_rB, w_wR_n;
wire w_ljmp, w_ljmp_dly, w_cis_ljmp;
wire [31:0] iword;
wire pf_valid;
 
 
reg [15:0] r_nxt_half;
 
generate if (OPT_CIS)
begin : SET_IWORD
 
assign iword = ((!i_instruction[`CISBIT])||(i_phase))
? i_instruction
: { 1'b1, i_instruction[14:0], i_instruction[15:0] };
 
end else begin : CLR_IWORD
 
assign iword = { 1'b0, i_instruction[30:0] };
 
end endgenerate
 
generate
if (OPT_EARLY_BRANCHING)
begin
if (OPT_CIS)
begin : CIS_EARLY_BRANCHING
 
assign w_cis_ljmp = (iword[31:16] == 16'hfcf8);
 
end else begin : NOCIS_EARLY_BRANCH
 
assign w_cis_ljmp = 1'b0;
 
end
 
assign w_ljmp = (iword == 32'h7c87c000);
 
end else begin : NO_EARLY_BRANCHING
 
assign w_cis_ljmp = 1'b0;
assign w_ljmp = 1'b0;
end endgenerate
 
reg [4:0] w_cis_op;
 
generate if (OPT_CIS)
begin : GEN_CIS_OP
 
always @(*)
if (!iword[`CISBIT])
w_cis_op = iword[26:22];
else case(iword[26:24])
3'h0: w_cis_op = 5'h00;
3'h1: w_cis_op = 5'h01;
3'h2: w_cis_op = 5'h02;
3'h3: w_cis_op = 5'h10;
3'h4: w_cis_op = 5'h12;
3'h5: w_cis_op = 5'h13;
3'h6: w_cis_op = 5'h18;
3'h7: w_cis_op = 5'h0d;
endcase
 
end else begin : GEN_NOCIS_OP
 
always @(*)
w_cis_op = w_op;
 
end endgenerate
 
// Decode instructions
assign w_op= iword[26:22];
assign w_mov = (w_cis_op == 5'h0d);
assign w_ldi = (w_cis_op[4:1] == 4'hc);
assign w_brev = (w_cis_op == 5'h08);
assign w_mpy = (w_cis_op[4:1] == 4'h5)||(w_cis_op[4:0]==5'h0c);
assign w_cmptst = (w_cis_op[4:1] == 4'h8);
assign w_ldilo = (w_cis_op[4:0] == 5'h09);
assign w_ALU = (!w_cis_op[4]) // anything with [4]==0, but ...
&&(w_cis_op[3:1] != 3'h7); // not the divide
assign w_add = (w_cis_op[4:0] == 5'h02);
assign w_mem = (w_cis_op[4:3] == 2'b10)&&(w_cis_op[2:1] !=2'b00);
assign w_sto = (w_mem)&&( w_cis_op[0]);
assign w_div = (!iword[`CISBIT])&&(w_op[4:1] == 4'h7);
assign w_fpu = (!iword[`CISBIT])&&(w_op[4:3] == 2'b11)
&&(w_dcdR[3:1] != 3'h7)&&(w_op[2:1] != 2'b00);
// If the result register is either CC or PC, and this would otherwise
// be a floating point instruction with floating point opcode of 0,
// then this is a NOOP.
assign w_special= (!iword[`CISBIT])&&((!OPT_FPU)||(w_dcdR[3:1]==3'h7))
&&(w_op[4:2] == 3'b111);
assign w_break = (w_special)&&(w_op[4:0]==5'h1c);
assign w_lock = (w_special)&&(w_op[4:0]==5'h1d);
assign w_sim = (w_special)&&(w_op[4:0]==5'h1e);
assign w_noop = (w_special)&&(w_op[4:0]==5'h1f);
 
 
// w_dcdR (4 LUTs)
//
// What register will we be placing results into (if at all)?
//
// Two parts to the result register: the register set, given for
// moves in iword[18] but only for the supervisor, and the other
// four bits encoded in the instruction.
//
assign w_dcdR = { ((!iword[`CISBIT])&&(w_mov)&&(!i_gie))?iword[`IMMSEL]:i_gie,
iword[30:27] };
 
// dcdB - What register is used in the opB?
//
assign w_dcdB[4] = ((!iword[`CISBIT])&&(w_mov)&&(!i_gie))?iword[13]:i_gie;
assign w_dcdB[3:0]= (iword[`CISBIT])
? (((!iword[`CISIMMSEL])&&(iword[26:25]==2'b10))
? `CPU_SP_REG : iword[22:19])
: iword[17:14];
 
// 0 LUTs
assign w_dcdA = w_dcdR; // on ZipCPU, A is always result reg
// 2 LUTs, 1 delay each
assign w_dcdR_pc = (w_dcdR == {i_gie, `CPU_PC_REG});
assign w_dcdR_cc = (w_dcdR == {i_gie, `CPU_CC_REG});
// 0 LUTs
assign w_dcdA_pc = w_dcdR_pc;
assign w_dcdA_cc = w_dcdR_cc;
// 2 LUTs, 1 delays each
assign w_dcdB_pc = (w_rB)&&(w_dcdB[3:0] == `CPU_PC_REG);
assign w_dcdB_cc = (w_rB)&&(w_dcdB[3:0] == `CPU_CC_REG);
 
//
// Under what condition will we execute this instruction? Only the
// load immediate instruction and the CIS instructions are completely
// unconditional. Well ... not quite. The BREAK, LOCK, and SIM/NOOP
// instructions are also unconditional.
//
assign w_cond = ((w_ldi)||(w_special)||(iword[`CISBIT])) ? 4'h8 :
{ (iword[21:19]==3'h0), iword[21:19] };
 
// rA - do we need to read register A?
assign w_rA = // Floating point reads reg A
((w_fpu)&&(OPT_FPU))
// Divide's read A
||(w_div)
// ALU ops read A,
// except for MOV's and BREV's which don't
||((w_ALU)&&(!w_brev)&&(!w_mov))
// STO's read A
||(w_sto)
// Test/compares
||(w_cmptst);
// rB -- do we read a register for operand B? Specifically, do we
// add the registers value to the immediate to create opB?
assign w_rB = (w_mov)
||((!iword[`CISBIT])&&(iword[`IMMSEL])&&(!w_ldi)&&(!w_special))
||(( iword[`CISBIT])&&(iword[`CISIMMSEL])&&(!w_ldi))
// If using compressed instruction sets,
// we *always* read on memory operands.
||(( iword[`CISBIT])&&(w_mem));
 
// wR -- will we be writing our result back?
// wR_n = !wR
// All but STO, NOOP/BREAK/LOCK, and CMP/TST write back to w_dcdR
assign w_wR_n = (w_sto)
||(w_special)
||(w_cmptst);
assign w_wR = !w_wR_n;
//
// wF -- do we write flags when we are done?
//
assign w_wF = (w_cmptst)
||((w_cond[3])&&(((w_fpu)&&(OPT_FPU))||(w_div)
||((w_ALU)&&(!w_mov)&&(!w_ldilo)&&(!w_brev)
&&(w_dcdR[3:1] != 3'h7))));
 
// Bottom 13 bits: no LUT's
// w_dcd[12: 0] -- no LUTs
// w_dcd[ 13] -- 2 LUTs
// w_dcd[17:14] -- (5+i0+i1) = 3 LUTs, 1 delay
// w_dcd[22:18] : 5 LUTs, 1 delay (assuming high bit is o/w determined)
wire [22:0] w_I, w_fullI;
wire w_Iz;
 
assign w_fullI = (w_ldi) ? { iword[22:0] } // LDI
// MOVE immediates have one less bit
:((w_mov) ?{ {(23-13){iword[12]}}, iword[12:0] }
// Normal Op-B immediate ... 18 or 14 bits
:((!iword[`IMMSEL]) ? { {(23-18){iword[17]}}, iword[17:0] }
: { {(23-14){iword[13]}}, iword[13:0] }
));
 
generate if (OPT_CIS)
begin : GEN_CIS_IMMEDIATE
wire [7:0] w_halfbits;
assign w_halfbits = iword[`CISIMMSEL:16];
 
wire [7:0] w_halfI;
assign w_halfI = (iword[26:24]==3'h6) ? w_halfbits[7:0] // 8'b for LDI
:(w_halfbits[7])?
{ {(6){w_halfbits[2]}}, w_halfbits[1:0]}
:{ w_halfbits[6], w_halfbits[6:0] };
assign w_I = (iword[`CISBIT])
? {{(23-8){w_halfI[7]}}, w_halfI }
: w_fullI;
 
end else begin : GEN_NOCIS_IMMEDIATE
 
assign w_I = w_fullI;
 
end endgenerate
 
assign w_Iz = (w_I == 0);
 
 
initial o_illegal = 1'b0;
always @(*)
begin
o_illegal <= 1'b0;
if ((!OPT_CIS)&&(i_instruction[`CISBIT]))
o_illegal <= 1'b1;
if ((!OPT_MPY)&&(w_mpy))
o_illegal <= 1'b1;
 
if ((!OPT_DIVIDE)&&(w_div))
o_illegal <= 1'b1;
else if ((OPT_DIVIDE)&&(w_div)&&(w_dcdR[3:1]==3'h7))
o_illegal <= 1'b1;
 
 
if ((!OPT_FPU)&&(w_fpu))
o_illegal <= 1'b1;
 
if ((!OPT_SIM)&&(w_sim))
// Simulation instructions on real hardware should
// always cause an illegal instruction error
o_illegal <= 1'b1;
 
// There are two (missing) special instructions
// These should cause an illegal instruction error
if ((w_dcdR[3:1]==3'h7)&&(w_cis_op[4:1]==4'b1101))
o_illegal <= 1'b1;
 
// If the lock function isn't implemented, this should
// also cause an illegal instruction error
if ((!OPT_LOCK)&&(w_lock))
o_illegal <= 1'b1;
end
 
generate if (OPT_OPIPE)
begin
// o_prepipe is true if a pipelined memory instruction
// might follow this one
assign o_prepipe =
((OPT_CIS)||(!i_instruction[`CISBIT]))
&&(o_M)&&(o_rB)
&&(o_dcdB[3:1] != 3'h7)
&&(o_dcdR[3:1] != 3'h7)
&&((!o_wR)||(o_dcdR != o_dcdB));
end else begin
assign o_prepipe = 1'b0;
end endgenerate
 
assign o_dcdR = { w_dcdR_cc, w_dcdR_pc, w_dcdR};
assign o_dcdA = { w_dcdA_cc, w_dcdA_pc, w_dcdA};
assign o_dcdB = { w_dcdB_cc, w_dcdB_pc, w_dcdB};
assign o_I = { {(32-22){w_I[22]}}, w_I[21:0] };
assign o_cond = w_cond;
assign o_wF = w_wF;
assign o_op = ((w_ldi)||(w_noop))? 4'hd : w_cis_op[3:0];
assign o_ALU = (w_ALU)||(w_ldi)||(w_cmptst)||(w_noop);
assign o_M = w_mem;
assign o_DV = (OPT_DIVIDE)&&(w_div);
assign o_FP = (OPT_FPU)&&(w_fpu);
assign o_break= w_break;
assign o_lock = (OPT_LOCK)&&(w_lock);
assign o_wR = w_wR;
assign o_rA = w_rA;
assign o_rB = w_rB;
assign o_sim = (OPT_SIM) ? ((w_sim)||(w_noop)) : 1'b0;
assign o_sim_immv = (OPT_SIM) ? iword[22:0] : 0;
 
endmodule
/formal/icontrol.sby
0,0 → 1,15
[options]
mode prove
depth 5
 
[engines]
smtbmc
 
[script]
read -formal -DICONTROL icontrol.v
read -formal -DICONTROL fwb_slave.v
prep -top icontrol
 
[files]
../../rtl/peripherals/icontrol.v
../../rtl/ex/fwb_slave.v
/formal/idecode.gtkw
0,0 → 1,173
[*]
[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
[*] Sun Dec 2 03:08:39 2018
[*]
[dumpfile] "(null)"
[savefile] "/home/dan/bizcopy/zipcpu/bench/formal/idecode.gtkw"
[timestart] 0
[size] 1665 600
[pos] -1 -1
*-3.760617 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 270
[signals_width] 230
[sst_expanded] 1
[sst_vpaned_height] 143
@28
idecode.i_ce
idecode.i_clk
idecode.i_gie
idecode.i_pf_valid
idecode.i_illegal
@22
idecode.i_instruction[31:0]
idecode.i_pc[25:0]
@28
idecode.i_reset
idecode.i_stalled
@22
idecode.iword[30:0]
@200
-
@29
idecode.o_valid
@22
idecode.o_dcdA[6:0]
idecode.o_dcdB[6:0]
@28
idecode.o_ALU
idecode.o_DV
idecode.o_FP
@22
idecode.o_I[31:0]
@28
idecode.o_M
@22
idecode.o_branch_pc[25:0]
@28
idecode.o_break
@22
idecode.o_cond[3:0]
@28
idecode.o_early_branch
idecode.o_early_branch_stb
idecode.o_illegal
idecode.o_ljmp
idecode.o_lock
@22
idecode.o_op[3:0]
idecode.o_pc[25:0]
@28
idecode.o_phase
idecode.o_pipe
@22
idecode.o_preA[4:0]
idecode.o_preB[4:0]
@28
idecode.o_rA
idecode.o_rB
idecode.o_sim
@22
idecode.o_sim_immv[22:0]
@28
idecode.o_wF
idecode.o_wR
idecode.o_zI
@22
idecode.f_hidden_state[31:0]
idecode.f_insn_word[31:0]
@28
idecode.f_last_insn
idecode.f_new_insn
idecode.f_past_valid
@22
idecode.f_result[127:0]
idecode.f_this_pipe_I[20:0]
@28
idecode.fc_ALU
idecode.fc_DV
idecode.fc_FP
@22
idecode.fc_I[31:0]
@28
idecode.fc_M
idecode.fc_break
@22
idecode.fc_cond[3:0]
idecode.fc_dcdA[6:0]
idecode.fc_dcdB[6:0]
idecode.fc_dcdR[6:0]
@28
idecode.fc_illegal
idecode.fc_lock
@22
idecode.fc_op[3:0]
@28
idecode.fc_rA
idecode.fc_rB
idecode.fc_sim
@22
idecode.fc_sim_immv[22:0]
@28
idecode.fc_wF
idecode.fc_wR
idecode.pf_valid
@22
idecode.possibly_unused[5:0]
idecode.r_I[22:0]
@28
idecode.r_valid
idecode.w_ALU
@22
idecode.w_I[22:0]
@28
idecode.w_Iz
idecode.w_add
idecode.w_break
idecode.w_brev
@22
idecode.w_cis_op[4:0]
@28
idecode.w_cmptst
@22
idecode.w_cond[3:0]
idecode.w_dcdA[4:0]
@28
idecode.w_dcdA_cc
idecode.w_dcdA_pc
@22
idecode.w_dcdB[4:0]
@28
idecode.w_dcdB_cc
idecode.w_dcdB_pc
@22
idecode.w_dcdR[4:0]
@28
idecode.w_dcdR_cc
idecode.w_dcdR_pc
idecode.w_div
idecode.w_fpu
@22
idecode.w_fullI[22:0]
@28
idecode.w_ldi
idecode.w_ldilo
idecode.w_ljmp
idecode.w_ljmp_dly
idecode.w_lock
idecode.w_mem
idecode.w_mov
idecode.w_mpy
idecode.w_noop
@22
idecode.w_op[4:0]
@28
idecode.w_rA
idecode.w_rB
idecode.w_sim
idecode.w_special
idecode.w_sto
idecode.w_wF
idecode.w_wR
idecode.w_wR_n
[pattern_trace] 1
[pattern_trace] 0
/formal/idecode.sby
0,0 → 1,40
[tasks]
pipe_div_mpy_cis_opipe pipelind div mpy cis pipemem
pipe_div_mpy_cis_nopipe pipelind div mpy cis nopipemem
pipe_div_mpy_nocis_pipe pipelind div mpy nocis pipemem
pipe_div_mpy_nocis_nopipe pipelind div mpy nocis nopipemem
pipe_div_nompy_nocis_nopipe pipelind div nompy nocis nopipemem
pipe_nodiv_nompy_nocis_nopipe pipelind nodiv nompy nocis nopipemem
nopipe_nodiv_nompy_nocis_nopipe nopipelind nodiv nompy nocis nopipemem
 
[options]
mode prove
depth 10
 
[engines]
smtbmc
 
[script]
read -formal -D IDECODE idecode.v
read -formal -D IDECODE f_idecode.v
 
nopipelind: chparam -set OPT_PIPELINED 0 idecode
pipelind: chparam -set OPT_PIPELINED 1 idecode
 
nodiv: chparam -set OPT_DIVIDE 0 idecode
div: chparam -set OPT_DIVIDE 1 idecode
 
nompy: chparam -set OPT_MPY 0 idecode
mpy: chparam -set OPT_MPY 1 idecode
 
nocis: chparam -set OPT_CIS 0 idecode
cis: chparam -set OPT_CIS 1 idecode
 
nopipemem: chparam -set OPT_OPIPE 0 idecode
pipemem: chparam -set OPT_OPIPE 1 idecode
 
prep -top idecode
 
[files]
../../rtl/core/idecode.v
f_idecode.v
/formal/mcve.sby
0,0 → 1,13
[options]
mode prove
depth 5
 
[engines]
smtbmc
 
[script]
read -formal mcve.v
prep -top mcve
 
[files]
mcve.v
/formal/mcve.v
0,0 → 1,22
module mcve(i_clk, o_val);
input wire i_clk;
output reg o_val;
parameter [0:0] THE_TEST = 1'b0;
 
generate if (THE_TEST)
begin
 
always @(*)
o_val = 1'b1;
 
always @(*)
assert(o_val);
 
end else begin
 
always @(*)
o_val = 1'b0;
 
end endgenerate
 
endmodule
/formal/memops.sby
0,0 → 1,20
[tasks]
cover
proof
 
[options]
proof: mode prove
cover: mode cover
 
[engines]
smtbmc
 
[script]
read -define MEMOPS
read -formal memops.v
read -formal fwb_master.v
prep -top memops
 
[files]
../../rtl/core/memops.v
../../rtl/ex/fwb_master.v
/formal/pfcache.gtkw
0,0 → 1,136
[*]
[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
[*] Mon Dec 10 22:22:31 2018
[*]
[dumpfile] "/home/dan/jericho/work/rnd/zipcpu/trunk/bench/formal/pfcache_cvr/engine_0/trace9.vcd"
[dumpfile_mtime] "Mon Dec 10 22:16:38 2018"
[dumpfile_size] 17974
[savefile] "/home/dan/jericho/work/rnd/zipcpu/trunk/bench/formal/pfcache.gtkw"
[timestart] 0
[size] 1762 600
[pos] -1 -1
*-4.197481 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 270
[signals_width] 254
[sst_expanded] 1
[sst_vpaned_height] 143
@28
pfcache.f_past_valid
pfcache.i_reset
pfcache.i_clear_cache
pfcache.i_clk
pfcache.i_new_pc
@22
pfcache.i_pc[31:0]
@28
pfcache.i_stall_n
pfcache.o_valid
pfcache.o_illegal
@22
pfcache.o_insn[31:0]
pfcache.o_pc[31:0]
@200
-
@28
[color] 2
pfcache.o_wb_cyc
[color] 2
pfcache.o_wb_stb
[color] 2
pfcache.o_wb_we
@22
[color] 2
pfcache.o_wb_addr[29:0]
[color] 2
pfcache.o_wb_data[31:0]
@28
[color] 2
pfcache.i_wb_stall
[color] 2
pfcache.i_wb_ack
@22
[color] 2
pfcache.i_wb_data[31:0]
@28
[color] 2
pfcache.i_wb_err
@200
-
@22
pfcache.f_const_addr[30:0]
pfcache.f_const_insn[31:0]
@28
[color] 3
pfcache.f_this_ack
[color] 3
pfcache.f_this_line
[color] 3
pfcache.f_this_tag
@200
-
@28
[color] 3
pfcache.f_this_pc
[color] 3
pfcache.f_this_data
[color] 3
pfcache.f_this_insn
@200
-
@22
pfcache.f_nreqs[3:0]
pfcache.f_nacks[3:0]
pfcache.f_outstanding[3:0]
@200
-
@28
pfcache.illegal_valid
@22
pfcache.illegal_cache[26:0]
@200
-
@28
pfcache.delay[1:0]
pfcache.bus_abort
pfcache.f_next_pc_v
@22
pfcache.f_cpu_delay[4:0]
pfcache.f_newpc_sreg[11:0]
pfcache.f_next_pc[31:0]
@28
pfcache.isrc
pfcache.last_ack
pfcache.last_addr
@22
pfcache.lastpc[31:0]
pfcache.lasttag[26:0]
@28
pfcache.needload
@22
pfcache.r_last_cache[31:0]
pfcache.r_lastpc[31:0]
@28
pfcache.r_new_request
@22
pfcache.r_pc[31:0]
pfcache.r_pc_cache[31:0]
@28
pfcache.r_v
pfcache.r_v_from_last
pfcache.r_v_from_pc
pfcache.rvsrc
pfcache.saddr[1:0]
pfcache.svmask
@22
pfcache.tagval[24:0]
pfcache.tagvalipc[24:0]
pfcache.tagvallst[24:0]
pfcache.valid_mask[3:0]
@28
pfcache.w_invalidate_result
pfcache.w_v_from_last
pfcache.w_v_from_pc
@23
pfcache.wraddr[4:0]
[pattern_trace] 1
[pattern_trace] 0
/formal/pfcache.sby
0,0 → 1,21
[tasks]
prf
cvr
 
[options]
prf: mode prove
prf: depth 5
cvr: mode cover
cvr: depth 60
 
[engines]
smtbmc
 
[script]
read -formal -DPFCACHE fwb_master.v
read -formal -DPFCACHE pfcache.v
prep -top pfcache
 
[files]
../../rtl/core/pfcache.v
../../rtl/ex/fwb_master.v
/formal/pipemem.sby
0,0 → 1,31
[tasks]
lcl_aligned_lock local_bus alignment_err lock
lcl_aligned_nolock local_bus alignment_err nolock
lcl_noaligned_lock local_bus noalignment_err lock
lcl_noaligned_nolock local_bus noalignment_err nolock
nolcl_aligned_lock nolocal_bus alignment_err lock
nolcl_aligned_nolock nolocal_bus alignment_err nolock
nolcl_noaligned_lock nolocal_bus noalignment_err lock
nolcl_noaligned_nolock nolocal_bus noalignment_err nolock
 
[options]
mode prove
depth 20
 
[engines]
smtbmc
 
[script]
read -formal -DPIPEMEM fwb_master.v
read -formal -DPIPEMEM pipemem.v
local_bus: chparam -set WITH_LOCAL_BUS 1 pipemem
nolocal_bus: chparam -set WITH_LOCAL_BUS 0 pipemem
alignment_err: chparam -set OPT_ALIGNMENT_ERR 1 pipemem
noalignment_err: chparam -set OPT_ALIGNMENT_ERR 0 pipemem
lock: chparam -set IMPLEMENT_LOCK 1 pipemem
nolock: chparam -set IMPLEMENT_LOCK 0 pipemem
prep -top pipemem
 
[files]
../../rtl/core/pipemem.v
../../rtl/ex/fwb_master.v
/formal/prefetch.sby
0,0 → 1,15
[options]
mode prove
depth 8
 
[engines]
smtbmc
 
[script]
read -formal -DPREFETCH fwb_master.v
read -formal -DPREFETCH prefetch.v
prep -top prefetch
 
[files]
../../rtl/core/prefetch.v
../../rtl/ex/fwb_master.v
/formal/wbdblpriarb.sby
0,0 → 1,17
[options]
mode prove
depth 4
 
[engines]
smtbmc
 
[script]
read -formal -D WBDBLPRIARB wbdblpriarb.v
read -formal -D WBDBLPRIARB fwb_master.v
read -formal -D WBDBLPRIARB fwb_slave.v
prep -top wbdblpriarb
 
[files]
../../rtl/ex/wbdblpriarb.v
../../rtl/ex/fwb_master.v
../../rtl/ex/fwb_slave.v
/formal/wbdmac.sby
0,0 → 1,17
[options]
mode prove
depth 12
 
[engines]
smtbmc
 
[script]
read -formal wbdmac.v
read -formal fwb_master.v
read -formal fwb_slave.v
prep -top wbdmac
 
[files]
../../rtl/peripherals/wbdmac.v
../../rtl/ex/fwb_master.v
../../rtl/ex/fwb_slave.v
/formal/wbpriarbiter.sby
0,0 → 1,18
[options]
mode prove
depth 5
 
[engines]
smtbmc
 
[script]
read -formal -D WBPRIARBITER wbpriarbiter.v
read -formal -D WBPRIARBITER fwb_master.v
read -formal -D WBPRIARBITER fwb_slave.v
prep -top wbpriarbiter
 
[files]
../../rtl/ex/wbpriarbiter.v
../../rtl/ex/fwb_master.v
../../rtl/ex/fwb_slave.v
 
/formal/wbwatchdog.sby
0,0 → 1,16
[options]
mode prove
depth 5
 
[engines]
smtbmc
 
[script]
read -formal wbwatchdog.v
read -formal fwb_slave.v
prep -top wbwatchdog
 
 
[files]
../../rtl/peripherals/wbwatchdog.v
../../rtl/ex/fwb_slave.v
/formal/zipcounter.sby
0,0 → 1,15
[options]
mode prove
depth 5
 
[engines]
smtbmc
 
[script]
read -formal -DZIPCOUNTER zipcounter.v
read -formal -DZIPCOUNTER fwb_slave.v
prep -top zipcounter
 
[files]
../../rtl/peripherals/zipcounter.v
../../rtl/ex/fwb_slave.v
/formal/zipcpu.gtkw
0,0 → 1,206
[*]
[*] GTKWave Analyzer v3.3.66 (w)1999-2015 BSI
[*] Wed May 9 22:36:52 2018
[*]
[dumpfile] "(null)"
[savefile] "/home/dan/work/rnd/zipcpu/trunk/bench/formal/zipcpu.gtkw"
[timestart] 0
[size] 1221 600
[pos] -1 -1
*-6.814017 90 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[treeopen] zipcpu.
[treeopen] zipcpu.instruction_decoder.
[sst_width] 196
[signals_width] 222
[sst_expanded] 1
[sst_vpaned_height] 155
@c00200
-External Inputs
@28
[color] 2
zipcpu.i_reset
[color] 2
zipcpu.i_clear_pf_cache
[color] 2
zipcpu.i_clk
[color] 2
zipcpu.i_halt
@22
[color] 2
zipcpu.i_dbg_data[31:0]
[color] 2
zipcpu.i_dbg_reg[4:0]
@28
[color] 2
zipcpu.i_dbg_we
@22
[color] 2
zipcpu.ipc[31:0]
@28
[color] 2
zipcpu.i_interrupt
@1401200
-External Inputs
@c00200
-CE
@28
zipcpu.dcd_ce
zipcpu.op_ce
zipcpu.master_ce
zipcpu.adf_ce_unconditional
zipcpu.alu_ce
zipcpu.div_ce
zipcpu.fpu_ce
zipcpu.mem_ce
@1401200
-CE
@c00200
-Valid
@28
zipcpu.pf_valid
zipcpu.dcd_valid
zipcpu.w_op_valid
zipcpu.op_valid
zipcpu.op_valid_alu
zipcpu.op_valid_div
zipcpu.op_valid_fpu
zipcpu.op_valid_mem
zipcpu.div_valid
zipcpu.alu_valid
zipcpu.mem_valid
zipcpu.mem_pc_valid
zipcpu.alu_pc_valid
@1401200
-Valid
@c00200
-Stall
@28
zipcpu.pf_stalled
zipcpu.dcd_A_stall
zipcpu.dcd_B_stall
zipcpu.dcd_F_stall
zipcpu.dcd_stalled
zipcpu.op_stall
zipcpu.master_stall
zipcpu.alu_stall
zipcpu.mem_pipe_stalled
zipcpu.mem_stalled
zipcpu.alu_sreg_stall
@1401200
-Stall
@c00200
-Busy
@28
zipcpu.alu_busy
zipcpu.mem_busy
zipcpu.mem_rdbusy
zipcpu.div_busy
@1401200
-Busy
@c00200
-f_instruction
@28
zipcpu.f_const_gie
@22
zipcpu.f_const_insn[31:0]
zipcpu.f_const_addr[31:0]
@28
zipcpu.f_const_phase
zipcpu.f_const_illegal
@1401200
-f_instruction
@c00200
-f_instruction_decoded
@28
zipcpu.fc_ALU
zipcpu.fc_DV
zipcpu.fc_FP
zipcpu.fc_M
zipcpu.fc_illegal
@22
zipcpu.fc_op[3:0]
@28
zipcpu.fc_wF
zipcpu.fc_wR
zipcpu.fc_rA
@22
zipcpu.fc_Aid[6:0]
@28
zipcpu.fc_rB
@22
zipcpu.fc_Bid[6:0]
zipcpu.fc_I[31:0]
zipcpu.fc_cond[3:0]
@28
zipcpu.fc_lock
zipcpu.fc_break
zipcpu.fc_sim
@22
zipcpu.fc_sim_immv[22:0]
@1401200
-f_instruction_decoded
@c00200
-f_insn_flags
@28
zipcpu.f_pf_insn
zipcpu.f_pre_dcd_insn
zipcpu.f_dcd_insn
zipcpu.f_op_insn
@1401200
-f_insn_flags
@c00200
-Prefetch
@28
zipcpu.pf_new_pc
zipcpu.pf_stalled
zipcpu.pf_valid
@22
zipcpu.pf_pc[31:0]
zipcpu.pf_instruction[31:0]
@28
zipcpu.pf_illegal
@1401200
-Prefetch
@22
zipcpu.op_opn[3:0]
zipcpu.op_Aid[4:0]
zipcpu.op_Bid[4:0]
@28
zipcpu.f_op_branch
zipcpu.dcd_early_branch
zipcpu.dcd_early_branch_stb
@22
zipcpu.dcd_opn[3:0]
@28
zipcpu.instruction_decoder.w_noop
zipcpu.instruction_decoder.w_special
zipcpu.instruction_decoder.w_cis_ljmp
zipcpu.instruction_decoder.w_div
@22
zipcpu.instruction_decoder.w_cis_op[4:0]
@28
zipcpu.instruction_decoder.w_cmptst
zipcpu.instruction_decoder.o_illegal
@22
zipcpu.instruction_decoder.w_dcdA[4:0]
@28
zipcpu.dcd_illegal
zipcpu.op_illegal
zipcpu.alu_illegal
zipcpu.pending_sreg_write
zipcpu.clear_pipeline
zipcpu.op_wR
zipcpu.set_cond
zipcpu.alu_wR
zipcpu.dcd_gie
zipcpu.gie
zipcpu.ill_err_i
zipcpu.alu_illegal
zipcpu.clear_pipeline
zipcpu.new_pc
zipcpu.pf_new_pc
zipcpu.wr_reg_ce
@22
zipcpu.wr_reg_id[4:0]
[pattern_trace] 1
[pattern_trace] 0
/formal/zipcpu.sby
0,0 → 1,89
[tasks]
dcache full_proof dcache
piped full_proof no_dcache
nopipe nopipe no_dcache
lowlogic nopipe no_dcache
ice40 nopipe no_dcache nobkram
 
[options]
mode prove
depth 18
dcache: depth 16 # Was 10
piped: depth 16 # Was 14 for yosys only, trying 18 w/ Verific
nopipe: depth 16 # Was 11
lowlogic: depth 16 # Was 10
ice40: depth 16 # Was 11
 
[engines]
smtbmc boolector
 
[script]
nobkram: read -define -DNO_DISTRIBUTED_RAM
read -define -DZIPCPU
#
read -formal -D ZIPCPU cpuops.v
read -formal -D ZIPCPU memops.v
read -formal -D ZIPCPU pipemem.v
read -formal -D ZIPCPU dcache.v
read -formal -D ZIPCPU iscachable.v
read -formal -D ZIPCPU idecode.v
read -formal -D ZIPCPU wbdblpriarb.v
#
read -formal -D ZIPCPU fwb_counter.v
read -formal -D ZIPCPU fwb_master.v
read -formal -D ZIPCPU fwb_slave.v
read -formal -D ZIPCPU f_idecode.v
read -formal -D ZIPCPU abs_prefetch.v
read -formal -D ZIPCPU abs_div.v
read -formal -D ZIPCPU abs_mpy.v
#
read -formal zipcpu.v
 
chparam -set IMPLEMENT_FPU 0 zipcpu
 
dcache:
chparam -set OPT_LGDCACHE 10 zipcpu
 
no_dcache:
chparam -set OPT_LGDCACHE 0 zipcpu
 
full_proof:
chparam -set IMPLEMENT_MPY 1 zipcpu
chparam -set IMPLEMENT_DIVIDE 1 zipcpu
chparam -set EARLY_BRANCHING 1 zipcpu
chparam -set OPT_CIS 1 zipcpu
chparam -set OPT_PIPELINED 1 zipcpu
 
nopipe:
chparam -set IMPLEMENT_MPY 0 zipcpu
chparam -set IMPLEMENT_DIVIDE 0 zipcpu
chparam -set EARLY_BRANCHING 0 zipcpu
chparam -set OPT_CIS 1 zipcpu
chparam -set OPT_PIPELINED 0 zipcpu
 
lowlogic:
chparam -set OPT_CIS 0 zipcpu
--
 
prep -top zipcpu
 
[files]
../../rtl/core/zipcpu.v
../../rtl/core/cpuops.v
../../rtl/core/memops.v
../../rtl/core/pipemem.v
../../rtl/core/dcache.v
../../rtl/core/iscachable.v
../../rtl/core/idecode.v
../../rtl/ex/wbdblpriarb.v
#
../../rtl/ex/fwb_counter.v
../../rtl/ex/fwb_master.v
../../rtl/ex/fwb_slave.v
#
../../rtl/cpudefs.v
f_idecode.v
abs_prefetch.v
abs_div.v
abs_mpy.v
#
/formal/zipjiffies.sby
0,0 → 1,15
[options]
mode prove
depth 5
 
[engines]
smtbmc
 
[script]
read -formal -DZIPJIFFIES zipjiffies.v
read -formal -DZIPJIFFIES fwb_slave.v
prep -top zipjiffies
 
[files]
../../rtl/peripherals/zipjiffies.v
../../rtl/ex/fwb_slave.v
/formal/zipmmu.gtkw
0,0 → 1,221
[*]
[*] GTKWave Analyzer v3.3.66 (w)1999-2015 BSI
[*] Mon Aug 27 21:59:16 2018
[*]
[dumpfile] "/home/dan/work/rnd/zipcpu/trunk/bench/formal/zipmmu.vcd"
[dumpfile_mtime] "Mon Aug 27 21:57:47 2018"
[dumpfile_size] 29996
[savefile] "/home/dan/work/rnd/zipcpu/trunk/bench/formal/zipmmu.gtkw"
[timestart] 0
[size] 1431 1028
[pos] -1 -1
*-5.031004 30 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 196
[signals_width] 190
[sst_expanded] 1
[sst_vpaned_height] 306
@28
zipmmu.i_reset
zipmmu.i_clk
zipmmu.i_gie
zipmmu.i_wbm_exe
@200
-
@28
zipmmu.i_wbm_cyc
zipmmu.i_wbm_stb
zipmmu.i_wbm_we
@22
zipmmu.i_wbm_addr[29:0]
zipmmu.i_wbm_data[31:0]
zipmmu.i_wbm_sel[3:0]
@28
[color] 3
zipmmu.o_rtn_stall
[color] 3
zipmmu.o_rtn_ack
@22
[color] 3
zipmmu.o_rtn_data[31:0]
@28
[color] 3
zipmmu.o_rtn_err
[color] 3
zipmmu.o_rtn_miss
@200
-
@28
zipmmu.i_wbs_cyc_stb
zipmmu.i_wbs_we
@22
zipmmu.i_wbs_addr[3:0]
zipmmu.i_wbs_data[31:0]
@28
zipmmu.o_wbs_ack
@22
zipmmu.o_wbs_data[31:0]
@28
zipmmu.o_wbs_stall
@200
-
@28
zipmmu.o_cyc
zipmmu.o_stb
zipmmu.o_we
@22
zipmmu.o_addr[27:0]
zipmmu.o_data[31:0]
zipmmu.o_sel[3:0]
@28
[color] 3
zipmmu.i_ack
[color] 3
zipmmu.i_stall
@22
[color] 3
zipmmu.i_data[31:0]
@28
[color] 3
zipmmu.i_err
@200
-
@22
[color] 1
zipmmu.fp_nacks[3:0]
[color] 1
zipmmu.fp_nreqs[3:0]
[color] 1
zipmmu.fp_outstanding[3:0]
@200
-
@23
[color] 1
zipmmu.fv_nacks[3:0]
[color] 1
zipmmu.fv_nreqs[3:0]
[color] 1
zipmmu.fv_outstanding[3:0]
@200
-
@28
zipmmu.adr_control
zipmmu.adr_ptable
zipmmu.adr_vtable
@22
zipmmu.bus_outstanding[5:0]
@28
zipmmu.bus_pending
zipmmu.cachable
zipmmu.exe_flag
zipmmu.exe_miss
@22
zipmmu.f_expected[3:0]
@28
zipmmu.f_kill_input
zipmmu.f_last_page[1:0]
zipmmu.f_past_gie
zipmmu.f_past_valid
zipmmu.f_past_wbm_cyc
@22
zipmmu.f_tlb_pipe[4:0]
@28
zipmmu.fp_is_zero
zipmmu.fv_is_one
zipmmu.kernel_context
zipmmu.last_exe
zipmmu.last_page_valid
@22
zipmmu.last_ppage[9:0]
@28
zipmmu.last_ro
zipmmu.last_tlb[1:0]
@22
zipmmu.last_vpage[11:0]
@28
zipmmu.miss_pending
zipmmu.pending_page_valid
zipmmu.pf_stb
zipmmu.pf_cachable
zipmmu.pf_return_cachable
@22
zipmmu.pf_return_p[9:0]
@28
zipmmu.pf_return_stb
@22
zipmmu.pf_return_v[11:0]
@28
zipmmu.pf_return_we
@22
zipmmu.ppage[9:0]
@200
-
@22
zipmmu.r_addr[29:0]
@28
zipmmu.r_context_word[1:0]
@22
zipmmu.r_data[31:0]
@28
zipmmu.r_exe
zipmmu.r_pending
@22
zipmmu.r_ppage[9:0]
zipmmu.r_sel[3:0]
zipmmu.r_tlb_match[3:0]
@28
zipmmu.r_valid
@22
zipmmu.r_vpage[11:0]
@28
zipmmu.r_we
zipmmu.ro_flag
zipmmu.ro_miss
zipmmu.rtn_err
@200
-
@28
zipmmu.s_pending
zipmmu.s_tlb_addr[1:0]
zipmmu.s_tlb_hit
zipmmu.s_tlb_miss
zipmmu.simple_miss
@22
zipmmu.status_word[31:0]
@28
zipmmu.table_err
zipmmu.this_page_valid
@22
zipmmu.tlb_accessed[3:0]
@28
zipmmu.tlb_cdata<0>[1:0]
zipmmu.tlb_cdata<1>[1:0]
zipmmu.tlb_cdata<2>[1:0]
zipmmu.tlb_cdata<3>[1:0]
zipmmu.tlb_flags<0>[2:0]
zipmmu.tlb_flags<1>[2:0]
zipmmu.tlb_flags<2>[2:0]
@22
zipmmu.tlb_pdata<0>[9:0]
zipmmu.tlb_pdata<1>[9:0]
zipmmu.tlb_pdata<2>[9:0]
zipmmu.tlb_valid[3:0]
zipmmu.tlb_vdata<0>[11:0]
zipmmu.tlb_vdata<1>[11:0]
zipmmu.tlb_vdata<2>[11:0]
zipmmu.tlb_vdata<3>[11:0]
zipmmu.unused[9:0]
@28
zipmmu.unused_data
@22
zipmmu.vpage[11:0]
zipmmu.w_control_data[31:0]
zipmmu.w_ptable_reg[29:0]
zipmmu.w_vtable_reg[31:0]
@28
zipmmu.wr_control
zipmmu.wr_ptable
zipmmu.wr_tlb_addr[1:0]
zipmmu.wr_vtable
zipmmu.z_context
[pattern_trace] 1
[pattern_trace] 0
/formal/zipmmu.sby
0,0 → 1,17
[options]
mode prove
depth 23
 
[engines]
smtbmc boolector
 
[script]
read -formal -D ZIPMMU zipmmu.v
read -formal -D ZIPMMU fwb_slave.v
read -formal -D ZIPMMU fwb_master.v
prep -top zipmmu
 
[files]
../../rtl/peripherals/zipmmu.v
../../rtl/ex/fwb_slave.v
../../rtl/ex/fwb_master.v
/formal/ziptimer.sby
0,0 → 1,15
[options]
mode prove
depth 5
 
[engines]
smtbmc
 
[script]
read -formal -DZIPTIMER ziptimer.v
read -formal -DZIPTIMER fwb_slave.v
prep -top ziptimer
 
[files]
../../rtl/peripherals/ziptimer.v
../../rtl/ex/fwb_slave.v
/formal
formal Property changes : Added: svn:ignore ## -0,0 +1,47 ## +busdelay +cpuops +dblfetch +dcache_bare +dcache_cover +dcache_cover_pipe +dcache_full +dcache_full_single +dcache_nolock_nolocal +dcache_nolock_system +dcache_piped +div +icontrol +idecode_nopipe_nodiv_nompy_nocis_nopipe +idecode_pipe_div_mpy_cis_nopipe +idecode_pipe_div_mpy_cis_opipe +idecode_pipe_div_mpy_nocis_nopipe +idecode_pipe_div_mpy_nocis_pipe +idecode_pipe_div_nompy_nocis_nopipe +idecode_pipe_nodiv_nompy_nocis_nopipe +memops_cover +memops_proof +pfcache_cvr +pfcache_prf +pipemem_lcl_aligned_lock +pipemem_lcl_aligned_nolock +pipemem_lcl_noaligned_lock +pipemem_lcl_noaligned_nolock +pipemem_nolcl_aligned_lock +pipemem_nolcl_aligned_nolock +pipemem_nolcl_noaligned_lock +pipemem_nolcl_noaligned_nolock +prefetch +wbdblpriarb +wbdmac +wbpriarbiter +wbwatchdog +zipcounter +zipcpu_dcache +zipcpu_ice40 +zipcpu_lowlogic +zipcpu_nopipe +zipcpu_piped +zipjiffies +zipmmu +ziptimer +*.ys Index: rtl/Makefile =================================================================== --- rtl/Makefile (nonexistent) +++ rtl/Makefile (revision 209) @@ -0,0 +1,64 @@ +################################################################################ +# +# Filename: Makefile +# +# Project: Zip CPU -- a small, lightweight, RISC CPU soft core +# +# Purpose: This makefile builds a verilator simulation of the rtl +# testbenches necessary to test certain components of the +# ZipSystem using Verilator. It does not make the system within Icarus, +# Vivado or Quartus. +# +# +# Creator: Dan Gisselquist, Ph.D. +# Gisselquist Technology, LLC +# +################################################################################ +# +# Copyright (C) 2015-2019, 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. +# +# License: GPL, v3, as defined and found on www.gnu.org, +# http://www.gnu.org/licenses/gpl.html +# +# +################################################################################ +# +.PHONY: all +all: zipmmu_tb + +CORED:= ../../rtl/core +PRPHD:= ../../rtl/peripherals +VOBJ := obj_dir +VERILATOR := verilator +VFLAGS := -Wall -MMD -trace -y $(PRPHD) -cc +SUBMAKE := $(MAKE) --no-print-directory -C + +$(VOBJ)/Vzipmmu_tb.cpp: $(PRPHD)/zipmmu.v zipmmu_tb.v memdev.v + $(VERILATOR) $(VFLAGS) zipmmu_tb.v +$(VOBJ)/Vzipmmu_tb.h: $(VOBJ)/Vzipmmu_tb.cpp + +$(VOBJ)/Vzipmmu_tb__ALL.a: $(VOBJ)/Vzipmmu_tb.cpp $(VOBJ)/Vzipmmu_tb.h + $(SUBMAKE) $(VOBJ) -f Vzipmmu_tb.mk + +.PHONY: zipmmu_tb +zipmmu_tb: $(VOBJ)/Vzipmmu_tb__ALL.a + +.PHONY: clean +clean: + rm -rf $(VOBJ) + + +DEPS := $(wildcard $(VOBJ)/*.d) +ifneq ($(DEPS),) +include $(DEPS) +endif Index: rtl/memdev.v =================================================================== --- rtl/memdev.v (nonexistent) +++ rtl/memdev.v (revision 209) @@ -0,0 +1,121 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: memdev.v +// +// Project: Zip CPU -- a small, lightweight, RISC CPU soft core +// +// Purpose: This file is really simple: it creates an on-chip memory, +// accessible via the wishbone bus, that can be used in this +// project. The memory has single cycle pipeline access, although the +// memory pipeline here still costs a cycle and there may be other cycles +// lost between the ZipCPU (or whatever is the master of the bus) and this, +// thus costing more cycles in access. Either way, operations can be +// pipelined for single cycle access on subsequent transactions. +// +// +// Creator: Dan Gisselquist, Ph.D. +// Gisselquist Technology, LLC +// +//////////////////////////////////////////////////////////////////////////////// +// +// Copyright (C) 2015-2019, 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 +// for a copy. +// +// License: GPL, v3, as defined and found on www.gnu.org, +// http://www.gnu.org/licenses/gpl.html +// +// +//////////////////////////////////////////////////////////////////////////////// +// +// +module memdev(i_clk, i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel, + o_wb_ack, o_wb_stall, o_wb_data); + parameter LGMEMSZ=15, DW=32, EXTRACLOCK= 0; + localparam AW = LGMEMSZ - 2; + input wire i_clk, i_wb_cyc, i_wb_stb, i_wb_we; + input wire [(AW-1):0] i_wb_addr; + input wire [(DW-1):0] i_wb_data; + input wire [(DW/8-1):0] i_wb_sel; + output reg o_wb_ack; + output wire o_wb_stall; + output reg [(DW-1):0] o_wb_data; + + wire w_wstb, w_stb; + wire [(DW-1):0] w_data; + wire [(AW-1):0] w_addr; + wire [(DW/8-1):0] w_sel; + + generate + if (EXTRACLOCK == 0) + begin + + assign w_wstb = (i_wb_stb)&&(i_wb_we); + assign w_stb = i_wb_stb; + assign w_addr = i_wb_addr; + assign w_data = i_wb_data; + assign w_sel = i_wb_sel; + + end else begin + + reg last_wstb, last_stb; + always @(posedge i_clk) + last_wstb <= (i_wb_stb)&&(i_wb_we); + always @(posedge i_clk) + last_stb <= (i_wb_stb); + + reg [(AW-1):0] last_addr; + reg [(DW-1):0] last_data; + reg [(DW/8-1):0] last_sel; + always @(posedge i_clk) + last_data <= i_wb_data; + always @(posedge i_clk) + last_addr <= i_wb_addr; + always @(posedge i_clk) + last_sel <= i_wb_sel; + + assign w_wstb = last_wstb; + assign w_stb = last_stb; + assign w_addr = last_addr; + assign w_data = last_data; + assign w_sel = last_sel; + end endgenerate + + reg [(DW-1):0] mem [0:((1<

powered by: WebSVN 2.1.0

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