Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: azonenberg/starshipraider
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 182ef455ed3e
Choose a base ref
...
head repository: azonenberg/starshipraider
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 3b673f99dc26
Choose a head ref
  • 3 commits
  • 16 files changed
  • 1 contributor

Commits on Jul 20, 2020

  1. Copy the full SHA
    8a60f9e View commit details
  2. Copy the full SHA
    148c792 View commit details
  3. Copy the full SHA
    3b673f9 View commit details
3 changes: 0 additions & 3 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -1,6 +1,3 @@
[submodule "bsp"]
path = bsp
url = https://github.com/azonenberg/antikernel-bsps
[submodule "rtl/antikernel-ipcores"]
path = rtl/antikernel-ipcores
url = git@github.com:azonenberg/antikernel-ipcores
1 change: 0 additions & 1 deletion bsp
Submodule bsp deleted from 279b0f
101 changes: 101 additions & 0 deletions rtl/MAXWELL/main-fpga/main-fpga.srcs/constrs_1/new/top.xdc
Original file line number Diff line number Diff line change
@@ -1,3 +1,94 @@
set_max_delay -from [get_cells [list network/mac/mac/sync_link_speed/sync_ack/sync/dout0_reg \
network/mac/mac/sync_link_speed/sync_en/sync/dout0_reg \
network/mac/rgmii_bridge/sync_link_speed/sync_ack/sync/dout0_reg \
network/mac/rgmii_bridge/sync_link_speed/sync_en/sync/dout0_reg \
network/stack/mac_sync/sync_ack/sync/dout0_reg \
network/stack/mac_sync/sync_en/sync/dout0_reg \
network/stack/rx_cdc/rx_cdc_fifo/sync_head/sync_ack/sync/dout0_reg \
network/stack/rx_cdc/rx_cdc_fifo/sync_head/sync_en/sync/dout0_reg \
network/stack/rx_cdc/rx_cdc_fifo/sync_tail/sync_ack/sync/dout0_reg \
network/stack/rx_cdc/rx_cdc_fifo/sync_tail/sync_en/sync/dout0_reg \
network/stack/sync_link_up/dout0_reg \
network/stack/tx_arbiter/arp_header_fifo/sync_head/sync_ack/sync/dout0_reg \
network/stack/tx_arbiter/arp_header_fifo/sync_head/sync_en/sync/dout0_reg \
network/stack/tx_arbiter/arp_header_fifo/sync_tail/sync_ack/sync/dout0_reg \
network/stack/tx_arbiter/arp_header_fifo/sync_tail/sync_en/sync/dout0_reg \
network/stack/tx_arbiter/arp_payload_fifo/sync_head/sync_ack/sync/dout0_reg \
network/stack/tx_arbiter/arp_payload_fifo/sync_head/sync_en/sync/dout0_reg \
network/stack/tx_arbiter/arp_payload_fifo/sync_tail/sync_ack/sync/dout0_reg \
network/stack/tx_arbiter/arp_payload_fifo/sync_tail/sync_en/sync/dout0_reg \
network/stack/tx_arbiter/ipv4_header_fifo/sync_head/sync_ack/sync/dout0_reg \
network/stack/tx_arbiter/ipv4_header_fifo/sync_head/sync_en/sync/dout0_reg \
network/stack/tx_arbiter/ipv4_header_fifo/sync_tail/sync_ack/sync/dout0_reg \
network/stack/tx_arbiter/ipv4_header_fifo/sync_tail/sync_en/sync/dout0_reg \
network/stack/tx_arbiter/ipv4_payload_fifo/sync_head/sync_ack/sync/dout0_reg \
network/stack/tx_arbiter/ipv4_payload_fifo/sync_head/sync_en/sync/dout0_reg \
network/stack/tx_arbiter/ipv4_payload_fifo/sync_tail/sync_ack/sync/dout0_reg \
network/stack/tx_arbiter/ipv4_payload_fifo/sync_tail/sync_en/sync/dout0_reg \
network/stack/tx_buf/header_fifo/sync_head/sync_ack/sync/dout0_reg \
network/stack/tx_buf/header_fifo/sync_head/sync_en/sync/dout0_reg \
network/stack/tx_buf/header_fifo/sync_tail/sync_ack/sync/dout0_reg \
network/stack/tx_buf/header_fifo/sync_tail/sync_en/sync/dout0_reg \
network/stack/tx_buf/payload_fifo/sync_head/sync_ack/sync/dout0_reg \
network/stack/tx_buf/payload_fifo/sync_head/sync_en/sync/dout0_reg \
network/stack/tx_buf/payload_fifo/sync_tail/sync_ack/sync/dout0_reg \
network/stack/tx_buf/payload_fifo/sync_tail/sync_en/sync/dout0_reg \
network/uart_bridge/rx_fifo/sync_head/sync_ack/sync/dout0_reg \
network/uart_bridge/rx_fifo/sync_head/sync_en/sync/dout0_reg \
network/uart_bridge/rx_fifo/sync_tail/sync_ack/sync/dout0_reg \
network/uart_bridge/rx_fifo/sync_tail/sync_en/sync/dout0_reg \
network/uart_bridge/sync_flush/sync/dout0_reg \
network/uart_bridge/tx_fifo/fifo/sync_rd_ptr/sync_ack/sync/dout0_reg \
network/uart_bridge/tx_fifo/fifo/sync_rd_ptr/sync_en/sync/dout0_reg \
network/uart_bridge/tx_fifo/fifo/sync_wr_ptr/sync_ack/sync/dout0_reg \
network/uart_bridge/tx_fifo/fifo/sync_wr_ptr/sync_en/sync/dout0_reg]] -to [get_cells [list network/mac/mac/sync_link_speed/sync_ack/sync/dout1_reg \
network/mac/mac/sync_link_speed/sync_en/sync/dout1_reg \
network/mac/rgmii_bridge/sync_link_speed/sync_ack/sync/dout1_reg \
network/mac/rgmii_bridge/sync_link_speed/sync_en/sync/dout1_reg \
network/stack/mac_sync/sync_ack/sync/dout1_reg \
network/stack/mac_sync/sync_en/sync/dout1_reg \
network/stack/rx_cdc/rx_cdc_fifo/sync_head/sync_ack/sync/dout1_reg \
network/stack/rx_cdc/rx_cdc_fifo/sync_head/sync_en/sync/dout1_reg \
network/stack/rx_cdc/rx_cdc_fifo/sync_tail/sync_ack/sync/dout1_reg \
network/stack/rx_cdc/rx_cdc_fifo/sync_tail/sync_en/sync/dout1_reg \
network/stack/sync_link_up/dout1_reg \
network/stack/tx_arbiter/arp_header_fifo/sync_head/sync_ack/sync/dout1_reg \
network/stack/tx_arbiter/arp_header_fifo/sync_head/sync_en/sync/dout1_reg \
network/stack/tx_arbiter/arp_header_fifo/sync_tail/sync_ack/sync/dout1_reg \
network/stack/tx_arbiter/arp_header_fifo/sync_tail/sync_en/sync/dout1_reg \
network/stack/tx_arbiter/arp_payload_fifo/sync_head/sync_ack/sync/dout1_reg \
network/stack/tx_arbiter/arp_payload_fifo/sync_head/sync_en/sync/dout1_reg \
network/stack/tx_arbiter/arp_payload_fifo/sync_tail/sync_ack/sync/dout1_reg \
network/stack/tx_arbiter/arp_payload_fifo/sync_tail/sync_en/sync/dout1_reg \
network/stack/tx_arbiter/ipv4_header_fifo/sync_head/sync_ack/sync/dout1_reg \
network/stack/tx_arbiter/ipv4_header_fifo/sync_head/sync_en/sync/dout1_reg \
network/stack/tx_arbiter/ipv4_header_fifo/sync_tail/sync_ack/sync/dout1_reg \
network/stack/tx_arbiter/ipv4_header_fifo/sync_tail/sync_en/sync/dout1_reg \
network/stack/tx_arbiter/ipv4_payload_fifo/sync_head/sync_ack/sync/dout1_reg \
network/stack/tx_arbiter/ipv4_payload_fifo/sync_head/sync_en/sync/dout1_reg \
network/stack/tx_arbiter/ipv4_payload_fifo/sync_tail/sync_ack/sync/dout1_reg \
network/stack/tx_arbiter/ipv4_payload_fifo/sync_tail/sync_en/sync/dout1_reg \
network/stack/tx_buf/header_fifo/sync_head/sync_ack/sync/dout1_reg \
network/stack/tx_buf/header_fifo/sync_head/sync_en/sync/dout1_reg \
network/stack/tx_buf/header_fifo/sync_tail/sync_ack/sync/dout1_reg \
network/stack/tx_buf/header_fifo/sync_tail/sync_en/sync/dout1_reg \
network/stack/tx_buf/payload_fifo/sync_head/sync_ack/sync/dout1_reg \
network/stack/tx_buf/payload_fifo/sync_head/sync_en/sync/dout1_reg \
network/stack/tx_buf/payload_fifo/sync_tail/sync_ack/sync/dout1_reg \
network/stack/tx_buf/payload_fifo/sync_tail/sync_en/sync/dout1_reg \
network/uart_bridge/rx_fifo/sync_head/sync_ack/sync/dout1_reg \
network/uart_bridge/rx_fifo/sync_head/sync_en/sync/dout1_reg \
network/uart_bridge/rx_fifo/sync_tail/sync_ack/sync/dout1_reg \
network/uart_bridge/rx_fifo/sync_tail/sync_en/sync/dout1_reg \
network/uart_bridge/sync_flush/sync/dout1_reg \
network/uart_bridge/tx_fifo/fifo/sync_rd_ptr/sync_ack/sync/dout1_reg \
network/uart_bridge/tx_fifo/fifo/sync_rd_ptr/sync_en/sync/dout1_reg \
network/uart_bridge/tx_fifo/fifo/sync_wr_ptr/sync_ack/sync/dout1_reg \
network/uart_bridge/tx_fifo/fifo/sync_wr_ptr/sync_en/sync/dout1_reg \
network/uart_bridge/uart/sync_rx/dout1_reg \
spi_iface/iface/sync_cs_n/dout1_reg \
spi_iface/iface/sync_mosi/dout1_reg \
spi_iface/iface/sync_sck/dout1_reg]] 3.200
set_property PACKAGE_PIN AB21 [get_ports {lsprobe_in_p[0]}]
set_property PACKAGE_PIN AE22 [get_ports {lsprobe_in_p[1]}]
set_property PACKAGE_PIN AF24 [get_ports {lsprobe_in_p[2]}]
@@ -214,6 +305,16 @@ create_generated_clock -name clk_200mhz -source [get_pins clocks/even_pll/mmcm/C
set_max_delay -datapath_only -from [get_cells -hierarchical *reg_a_ff*] -to [get_cells -hierarchical *reg_b_reg*] 3.200

set_max_delay -from [get_cells -hierarchical *dout0_reg*] -to [get_cells -hierarchical *dout1_reg*] 3.200

create_pblock pblock_network
add_cells_to_pblock [get_pblocks pblock_network] [get_cells -quiet [list network]]
resize_pblock [get_pblocks pblock_network] -add {CLOCKREGION_X0Y2:CLOCKREGION_X0Y4}
create_pblock pblock_trigger
add_cells_to_pblock [get_pblocks pblock_trigger] [get_cells -quiet [list trig]]
resize_pblock [get_pblocks pblock_trigger] -add {CLOCKREGION_X0Y0:CLOCKREGION_X0Y1}
create_pblock pblock_ddr
add_cells_to_pblock [get_pblocks pblock_ddr] [get_cells -quiet [list ddr_controller]]
resize_pblock [get_pblocks pblock_ddr] -add {CLOCKREGION_X1Y0:CLOCKREGION_X1Y2}
set_property C_CLK_INPUT_FREQ_HZ 300000000 [get_debug_cores dbg_hub]
set_property C_ENABLE_CLK_DIVIDER false [get_debug_cores dbg_hub]
set_property C_USER_SCAN_CHAIN 1 [get_debug_cores dbg_hub]
1 change: 1 addition & 0 deletions rtl/MAXWELL/main-fpga/main-fpga.srcs/formal_1/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
*/*
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
[options]
mode prove
depth 50

[engines]
smtbmc z3

[script]
read -formal SPIRegisterInterface_formal.sv
read -formal SPIHostInterface.sv
read -formal SPIRegisterInterface.sv
read -formal SPIDeviceInterface.sv
read -formal ThreeStageSynchronizer.sv
prep -top SPIRegisterInterface_formal

[files]
SPIRegisterInterface_formal.sv
../sources_1/new/SPIRegisterInterface.sv
../../../../antikernel-ipcores/interface/spi/SPIHostInterface.sv
../../../../antikernel-ipcores/interface/spi/SPIDeviceInterface.sv
../../../../antikernel-ipcores/clock/crossing/ThreeStageSynchronizer.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,224 @@
`default_nettype none
`timescale 1ns/1ps
/***********************************************************************************************************************
* *
* STARSHIPRAIDER v0.1 *
* *
* Copyright (c) 2012-2020 Andrew D. Zonenberg *
* All rights reserved. *
* *
* Redistribution and use in source and binary forms, with or without modification, are permitted provided that the *
* following conditions are met: *
* *
* * Redistributions of source code must retain the above copyright notice, this list of conditions, and the *
* following disclaimer. *
* *
* * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the *
* following disclaimer in the documentation and/or other materials provided with the distribution. *
* *
* * Neither the name of the author nor the names of any contributors may be used to endorse or promote products *
* derived from this software without specific prior written permission. *
* *
* THIS SOFTWARE IS PROVIDED BY THE AUTHORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL *
* THE AUTHORS BE HELD LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES *
* (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR *
* BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT *
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *
* POSSIBILITY OF SUCH DAMAGE. *
* *
***********************************************************************************************************************/

/**
@file
@author Andrew D. Zonenberg
@brief Formal testbench for SPIRegisterInterface
*/
module SPIRegisterInterface_formal(
input wire clk,

input wire wr_en,
input wire[15:0] wr_addr,
input wire[31:0] wr_data
);

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Generate SPI transactions when a write happens

typedef enum logic[3:0]
{
TX_STATE_IDLE = 0,
TX_STATE_ADDR_0 = 1,
TX_STATE_ADDR_1 = 2,
TX_STATE_DATA_0 = 3,
TX_STATE_DATA_1 = 4,
TX_STATE_DATA_2 = 5,
TX_STATE_DATA_3 = 6,
TX_STATE_DONE = 7,
TX_STATE_WAIT = 8
} txstate_t;
txstate_t tx_state = TX_STATE_IDLE;

logic cs_n = 1;

logic shift_en = 0;
wire shift_done;
logic[7:0] tx_data = 0;

logic[15:0] wr_addr_saved = 0;
logic[31:0] wr_data_saved = 0;

//Input constraints
always_comb begin

//Cannot start a new transaction if one is in progress
if(tx_state != TX_STATE_IDLE)
assume(!wr_en);

//Don't change data when a transaction is active
if(!wr_en) begin
assume(wr_addr == wr_addr_saved);
assume(wr_data == wr_data_saved);
end

end

always_ff @(posedge clk) begin

shift_en <= 0;

case(tx_state)

//Wait for stuff to happen
TX_STATE_IDLE: begin

if(wr_en) begin
cs_n <= 0;
tx_state <= TX_STATE_ADDR_0;

wr_data_saved <= wr_data;
wr_addr_saved <= wr_addr;
end

end //end TX_STATE_IDLE

//Send the address
TX_STATE_ADDR_0: begin
shift_en <= 1;
tx_data <= wr_addr[15:8];
tx_state <= TX_STATE_ADDR_1;
end //end TX_STATE_ADDR_0

TX_STATE_ADDR_1: begin
if(shift_done) begin
shift_en <= 1;
tx_data <= wr_addr[7:0];
tx_state <= TX_STATE_DATA_0;
end
end //end TX_STATE_ADDR_0

//Send the data
TX_STATE_DATA_0: begin
if(shift_done) begin
shift_en <= 1;
tx_data <= wr_addr[31:24];
tx_state <= TX_STATE_DATA_1;
end
end //end TX_STATE_DATA_0

TX_STATE_DATA_1: begin
if(shift_done) begin
shift_en <= 1;
tx_data <= wr_addr[23:16];
tx_state <= TX_STATE_DATA_2;
end
end //end TX_STATE_DATA_1

TX_STATE_DATA_2: begin
if(shift_done) begin
shift_en <= 1;
tx_data <= wr_addr[15:8];
tx_state <= TX_STATE_DATA_3;
end
end //end TX_STATE_DATA_2

TX_STATE_DATA_3: begin
if(shift_done) begin
shift_en <= 1;
tx_data <= wr_addr[7:0];
tx_state <= TX_STATE_DONE;
end
end //end TX_STATE_DATA_3

TX_STATE_DONE: begin
if(shift_done) begin
cs_n <= 1;
tx_state <= TX_STATE_WAIT;
end
end //end TX_STATE_DONE

//Wait for the slave to finish processing the transaction
TX_STATE_WAIT: begin
if(reg_wr_en)
tx_state <= TX_STATE_IDLE;
end //end TX_STATE_WAIT

endcase

end

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// SPI host controller for translating external native memory interface to SPI transactions

wire sck;
wire mosi;
wire miso;

SPIHostInterface host(
.clk(clk),
.clkdiv(4),

.spi_sck(sck),
.spi_mosi(mosi),
.spi_miso(miso),

.shift_en(shift_en),
.shift_done(shift_done),
.tx_data(tx_data),
.rx_data()
);

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// The actual DUT

wire reg_wr_en;
wire[15:0] reg_wr_addr;
wire[31:0] reg_wr_data;

SPIRegisterInterface dut(
.clk_312mhz(clk),

.mcu_spi_cs_n(cs_n),
.mcu_spi_sck(sck),
.mcu_spi_mosi(mosi),
.mcu_spi_miso(miso),

.reg_wr_en(reg_wr_en),
.reg_wr_addr(reg_wr_addr),
.reg_wr_data(reg_wr_data)
);

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Verification logic

always_ff @(posedge clk) begin

//When we get a write, make sure it's correct
if(reg_wr_en) begin
assert(wr_addr == reg_wr_addr);
assert(wr_data == reg_wr_data);
end

end

endmodule
Loading