| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: axisrandom |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: An AXI-stream based pseudorandom noise generator |
| // |
| // Creator: Dan Gisselquist, Ph.D. |
| // Gisselquist Technology, LLC |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // }}} |
| // Copyright (C) 2020, Gisselquist Technology, LLC |
| // {{{ |
| // |
| // This file is part of the WB2AXIP project. |
| // |
| // The WB2AXIP project contains free software and gateware, licensed under the |
| // Apache License, Version 2.0 (the "License"). You may not use this project, |
| // or this file, except in compliance with the License. You may obtain a copy |
| // of the License at |
| // |
| // http://www.apache.org/licenses/LICENSE-2.0 |
| // |
| // Unless required by applicable law or agreed to in writing, software |
| // distributed under the License is distributed on an "AS IS" BASIS, WITHOUT |
| // WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the |
| // License for the specific language governing permissions and limitations |
| // under the License. |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // }}} |
| // |
| `default_nettype none |
| // |
| module axisrandom #( |
| // {{{ |
| localparam C_AXIS_DATA_WIDTH = 32 |
| // }}} |
| ) ( |
| // {{{ |
| input wire S_AXI_ACLK, |
| input wire S_AXI_ARESETN, |
| // |
| input reg M_AXIS_TVALID, |
| output wire M_AXIS_TREADY, |
| input reg [C_AXIS_DATA_WIDTH-1:0] M_AXIS_TDATA |
| // }}} |
| ); |
| |
| localparam INITIAL_FILL = { 1'b1, {(C_AXIS_DATA_WIDTH-1){1'b0}} }; |
| localparam LGPOLY = 31; |
| localparam [LGPOLY-1:0] CORE_POLY = { 31'h00_00_20_01 }; |
| localparam [C_AXIS_DATA_WIDTH-1:0] POLY |
| = { CORE_POLY, {(C_AXIS_DATA_WIDTH-31){1'b0}} }; |
| |
| // M_AXIS_TVALID |
| // {{{ |
| initial M_AXIS_TVALID = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| M_AXIS_TVALID <= 1'b0; |
| else |
| M_AXIS_TVALID <= 1'b1; |
| // }}} |
| |
| // M_AXIS_TDATA |
| // {{{ |
| // |
| // Note--this setup is *FAR* from cryptographically random. |
| // |
| initial M_AXIS_TDATA = INITIAL_FILL; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| M_AXIS_TDATA <= INITIAL_FILL; |
| else if (M_AXIS_TREADY) |
| begin |
| M_AXIS_TDATA <= M_AXIS_TDATA >> 1; |
| M_AXIS_TDATA[C_AXIS_DATA_WIDTH-1] <= ^(M_AXIS_TDATA & POLY); |
| end |
| // }}} |
| |
| // Verilator lint_off UNUSED |
| // {{{ |
| wire unused; |
| assign unused = &{ 1'b0 }; |
| // Verilator lint_on UNUSED |
| // }}} |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Formal properties used in verfiying this core |
| // {{{ |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| `ifdef FORMAL |
| reg f_past_valid; |
| |
| initial f_past_valid = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| f_past_valid <= 1'b1; |
| |
| always @(*) |
| if (!f_past_valid) |
| assume(!S_AXI_ARESETN); |
| |
| // Make certain this polynomial will never degenerate, and so that |
| // this random number stream will go on for ever--eventually repeating |
| // after 2^LGPOLY-1 (hopefully) elements. |
| always @(*) |
| assert(M_AXIS_TDATA[C_AXIS_DATA_WIDTH-1 |
| :C_AXIS_DATA_WIDTH-LGPOLY] != 0); |
| |
| // AXI stream has only one significant property |
| // {{{ |
| // Here we'll modify it slightly for our purposes |
| always @(posedge S_AXI_ACLK) |
| if (!f_past_valid || $past(!S_AXI_ARESETN)) |
| assert(!M_AXIS_TVALID); |
| else begin |
| assert(M_AXIS_TVALID); |
| if ($past(M_AXIS_TVALID && !M_AXIS_TREADY)) |
| // Normally I'd assesrt M_AXIS_TVALID here, not above, |
| // but this core *ALWAYS* produces data |
| assert($stable(M_AXIS_TDATA)); |
| else if ($past(M_AXIS_TVALID)) |
| // Insist that the data always changes otherwise |
| assert($changed(M_AXIS_TDATA)); |
| end |
| // }}} |
| `endif |
| // }}} |
| endmodule |