diff options
Diffstat (limited to 'testsuite/ghdl-issues/issue1309')
| -rw-r--r-- | testsuite/ghdl-issues/issue1309/axis_squarer.sby | 34 | ||||
| -rw-r--r-- | testsuite/ghdl-issues/issue1309/axis_squarer.vhd | 114 | ||||
| -rw-r--r-- | testsuite/ghdl-issues/issue1309/faxis_master.v | 230 | ||||
| -rw-r--r-- | testsuite/ghdl-issues/issue1309/faxis_slave.v | 230 | ||||
| -rw-r--r-- | testsuite/ghdl-issues/issue1309/tb_formal_top.v | 131 | ||||
| -rwxr-xr-x | testsuite/ghdl-issues/issue1309/testsuite.sh | 10 |
6 files changed, 749 insertions, 0 deletions
diff --git a/testsuite/ghdl-issues/issue1309/axis_squarer.sby b/testsuite/ghdl-issues/issue1309/axis_squarer.sby new file mode 100644 index 0000000..c72c50d --- /dev/null +++ b/testsuite/ghdl-issues/issue1309/axis_squarer.sby @@ -0,0 +1,34 @@ +[tasks] +verify_bmc +prove +cover + +[options] +verify_bmc: mode bmc +verify_bmc: depth 40 +prove: mode prove +prove: depth 20 +cover: mode cover +cover: depth 40 + +[engines] +smtbmc z3 parallel.enable=true + +[script] +ghdl axis_squarer.vhd -e axis_squarer +read_verilog -formal faxis_master.v +read_verilog -formal faxis_slave.v +read_verilog -formal tb_formal_top.v +--pycode-begin-- +cmd = "hierarchy -top tb_formal_top" +if "cover" in tags: + cmd += " -chparam no_backpressure 1" +output(cmd); +--pycode-end-- +prep -top tb_formal_top + +[files] +axis_squarer.vhd +faxis_master.v +faxis_slave.v +tb_formal_top.v diff --git a/testsuite/ghdl-issues/issue1309/axis_squarer.vhd b/testsuite/ghdl-issues/issue1309/axis_squarer.vhd new file mode 100644 index 0000000..49cb1fa --- /dev/null +++ b/testsuite/ghdl-issues/issue1309/axis_squarer.vhd @@ -0,0 +1,114 @@ +---------------------------------------------------------------------------------- +-- Company: +-- Engineer: +-- +-- Create Date: 04/08/2020 11:41:37 AM +-- Design Name: +-- Module Name: axis_squarer - Behavioral +-- Project Name: +-- Target Devices: +-- Tool Versions: +-- Description: +-- +-- Dependencies: +-- +-- Revision: +-- Revision 0.01 - File Created +-- Additional Comments: +-- +---------------------------------------------------------------------------------- + + +library IEEE; +use IEEE.STD_LOGIC_1164.ALL; + +-- Uncomment the following library declaration if using +-- arithmetic functions with Signed or Unsigned values +use IEEE.NUMERIC_STD.ALL; + +-- Uncomment the following library declaration if instantiating +-- any Xilinx leaf cells in this code. +--library UNISIM; +--use UNISIM.VComponents.all; + +entity axis_squarer is + Port ( clk : in STD_LOGIC; + aresetn : in STD_LOGIC; + s_axis_tdata : in STD_LOGIC_VECTOR (31 downto 0); + s_axis_tlast : in STD_LOGIC; + s_axis_tvalid : in STD_LOGIC; + s_axis_tready : out STD_LOGIC; + + m_axis_tdata : out STD_LOGIC_VECTOR (31 downto 0); + m_axis_tlast : out STD_LOGIC; + m_axis_tvalid : out STD_LOGIC; + m_axis_tready : in STD_LOGIC); +end axis_squarer; + +architecture Behavioral of axis_squarer is + signal idle_counter: UNSIGNED(7 downto 0) := (others => '0'); + signal counter_start_long: UNSIGNED(3 downto 0) := (others => '0'); + type FSM_STATES is (IDLE, TX_RESULT, LONG_COMPUTATION); + signal fsm: FSM_STATES := IDLE; +begin + fsm_main: process(clk) is + begin + if rising_edge(clk) then + if aresetn = '0' then + fsm <= IDLE; + -- Reset stuff added below in response to fv + m_axis_tlast <= '0'; + counter_start_long <= (others => '0'); + else + case fsm is + when IDLE => + -- Wait for input valid, then put data onto output bus + if s_axis_tvalid = '1' then + m_axis_tdata <= not s_axis_tdata; + if s_axis_tlast = '1' or counter_start_long = 2 then + m_axis_tlast <= '1'; + else + m_axis_tlast <= '0'; + end if; + fsm <= TX_RESULT; + end if; + when TX_RESULT => + -- Wait for output ready + -- Do 8 fast returns before a single slow return + if m_axis_tready = '1' then + m_axis_tlast <= '0'; + counter_start_long <= counter_start_long+1; + if counter_start_long = 2 then + fsm <= LONG_COMPUTATION; + counter_start_long <= (others => '0'); + else + fsm <= IDLE; + end if; + end if; + when LONG_COMPUTATION => + -- Wait for 16 cycles + -- In actuality a longer computation goes here but simplify by reducing it to a wait + idle_counter <= idle_counter + 1; + if idle_counter = 5 then + fsm <= IDLE; + end if; + end case; + end if; + end if; + end process; + + fsm_axis_handshake_outputs: process(fsm,aresetn) is + begin + case fsm is + when IDLE => + s_axis_tready <= aresetn; -- Ready when not reset + m_axis_tvalid <= '0'; + when TX_RESULT => + s_axis_tready <= '0'; + m_axis_tvalid <= '1'; + when LONG_COMPUTATION => + s_axis_tready <= '0'; + m_axis_tvalid <= '0'; + end case; + end process; +end Behavioral; diff --git a/testsuite/ghdl-issues/issue1309/faxis_master.v b/testsuite/ghdl-issues/issue1309/faxis_master.v new file mode 100644 index 0000000..ae31735 --- /dev/null +++ b/testsuite/ghdl-issues/issue1309/faxis_master.v @@ -0,0 +1,230 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: faxis_master.v +// +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: Formal properties for verifying the proper functionality of an +// AXI Stream master. +// +// Creator: Dan Gisselquist, Ph.D. +// Gisselquist Technology, LLC +// +//////////////////////////////////////////////////////////////////////////////// +// +// Copyright (C) 2019-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 faxis_master #( + parameter F_MAX_PACKET = 0, + parameter F_MIN_PACKET = 0, + parameter F_MAX_STALL = 0, + parameter C_S_AXI_DATA_WIDTH = 32, + parameter C_S_AXI_ID_WIDTH = 1, + parameter C_S_AXI_ADDR_WIDTH = 1, + parameter C_S_AXI_USER_WIDTH = 1, + parameter [0:0] OPT_ASYNC_RESET = 1'b0, + // + // F_LGDEPTH is the number of bits necessary to represent a packets + // length + parameter F_LGDEPTH = 32, + // + localparam AW = C_S_AXI_ADDR_WIDTH, + localparam DW = C_S_AXI_DATA_WIDTH, + localparam IDW = C_S_AXI_ID_WIDTH, + localparam UW = C_S_AXI_USER_WIDTH + // + ) ( + // + input wire i_aclk, i_aresetn, + input wire i_tvalid, + input wire i_tready = 1, + input wire [DW-1:0] i_tdata, + input wire [DW/8-1:0] i_tstrb = {(DW/8){1'b1}}, + input wire [DW/8-1:0] i_tkeep = {(DW/8){1'b1}}, + input wire i_tlast, + input wire [(IDW>0?IDW:1)-1:0] i_tid = {(IDW){1'b0}}, + input wire [(AW>0?AW:1)-1:0] i_tdest = {(AW){1'b0}}, + input wire [(UW>0?UW:1)-1:0] i_tuser = {(UW){1'b0}}, + // + output reg [F_LGDEPTH-1:0] f_bytecount, + //(* anyconst *) output reg [AW+IDW-1:0] f_routecheck + ); + +`define SLAVE_ASSUME assert +`define SLAVE_ASSERT assume + + localparam F_STALLBITS = (F_MAX_STALL <= 1) + ? 1 : $clog2(F_MAX_STALL+2); + reg f_past_valid; + reg [F_LGDEPTH-1:0] f_vbytes; + reg [F_STALLBITS-1:0] f_stall_count; + integer iB; + genvar k; + + // + // f_past_valid is used to make certain that temporal assertions + // depending upon past values depend upon *valid* past values. + // It is true for all clocks other than the first clock. + initial f_past_valid = 1'b0; + always @(posedge i_aclk) + f_past_valid <= 1'b1; + + // + // Reset should always be active (low) initially + always @(posedge i_aclk) + if (!f_past_valid) + `SLAVE_ASSUME(!i_aresetn); + + // + // During and following a reset, TVALID should be deasserted + always @(posedge i_aclk) + if ((!f_past_valid)||(!i_aresetn && OPT_ASYNC_RESET)||($past(!i_aresetn))) + `SLAVE_ASSUME(!i_tvalid); + + // + // If TVALID but not TREADY, then the master isn't allowed to change + // anything until the slave asserts TREADY. + always @(posedge i_aclk) + if ((f_past_valid)&&($past(i_aresetn))&&(!OPT_ASYNC_RESET || i_aresetn) + &&($past(i_tvalid))&&(!$past(i_tready))) + begin + `SLAVE_ASSUME(i_tvalid); + `SLAVE_ASSUME($stable(i_tstrb)); + `SLAVE_ASSUME($stable(i_tkeep)); + `SLAVE_ASSUME($stable(i_tlast)); + //`SLAVE_ASSUME($stable(i_tid)); + //`SLAVE_ASSUME($stable(i_tdest)); + //`SLAVE_ASSUME($stable(i_tuser)); + end + + generate for(k=0; k<DW/8; k=k+1) + begin : CHECK_PARTIAL_DATA + + // If TVALID && !TREADY, only those TDATA values with TKEEP + // high are required to maintain their values until TREADY + // becomes true. + always @(posedge i_aclk) + if ((f_past_valid)&&($past(i_aresetn)) + &&(!OPT_ASYNC_RESET || i_aresetn) + &&($past(i_tvalid))&&(!$past(i_tready))) + begin + if (i_tkeep[k]) + `SLAVE_ASSUME($stable(i_tdata[k*8 +: 8])); + // else this is a null (don't care) byte, with + // no data within it + // + end + + end endgenerate + + // + // TKEEP == LOW and TSTRB == HIGH is reserved per the spec, and + // must not be used + always @(posedge i_aclk) + if (i_tvalid) + `SLAVE_ASSUME((~i_tkeep & i_tstrb)==0); + + // + // f_vbytes is the number of valid bytes contained in the current beat + // It is used for counting packet lengths below. + always @(*) + if (!i_tvalid) + f_vbytes = 0; + else begin + f_vbytes = 0; + for(iB=0; iB < DW/8; iB=iB+1) + if (i_tkeep[iB] && i_tstrb[iB]) + f_vbytes = f_vbytes + 1; + end + + // + // f_bytecount is the number of bytes that have taken place so far in + // the current packet transmission. Note that we are *only* counting + // our location within the stream if the TUSER and TDEST fields match + // our (solver chosen) ROUTECHECK. That way we don't have to check + // *EVERY POSSIBLE* TUSER and TDEST combination. + initial f_bytecount = 0; + always @(posedge i_aclk) + if (!i_aresetn) + f_bytecount <= 0; + else if (i_tready && i_tvalid /*&& ({ i_tuser, i_tdest } == f_routecheck)*/) + begin + if (i_tlast) + f_bytecount <= 0; + else + f_bytecount <= f_bytecount + f_vbytes; + end + + // + // Count the number of clock cycles between ready's. We'll use this in + // a bit to insist on an (optional) minimum transfer speed. + initial f_stall_count = 0; + always @(posedge i_aclk) + if (!i_aresetn || !i_tvalid || i_tready) + f_stall_count <= 0; + else if (!(&f_stall_count)) + f_stall_count <= f_stall_count + 1; + + // + // F_MAX_PACKET + // + // An optional check, to make certain packets don't exceed some maximum + // length + generate if (F_MAX_PACKET > 0) + begin : MAX_PACKET + + always @(*) + `SLAVE_ASSUME(f_bytecount + f_vbytes <= F_MAX_PACKET); + + end endgenerate + + // + // F_MIN_PACKET + // + // An optoinal check, forcing a minimum packet length + generate if (F_MIN_PACKET > 0) + begin : MIN_PACKET + + always @(*) + if (i_tvalid && i_tlast) + `SLAVE_ASSUME(f_bytecount + f_vbytes >= F_MIN_PACKET); + + end endgenerate + + // + // F_MAX_STALL + // + // Another optional check, this time insisting that the READY flag can + // only be low for up to F_MAX_STALL clocks. + // + generate if (F_MAX_STALL > 0) + begin : MAX_STALL_CHECK + + always @(*) + `SLAVE_ASSERT(f_stall_count < F_MAX_STALL); + + end endgenerate +endmodule +`undef SLAVE_ASSUME +`undef SLAVE_ASSERT + diff --git a/testsuite/ghdl-issues/issue1309/faxis_slave.v b/testsuite/ghdl-issues/issue1309/faxis_slave.v new file mode 100644 index 0000000..c350e8b --- /dev/null +++ b/testsuite/ghdl-issues/issue1309/faxis_slave.v @@ -0,0 +1,230 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: faxis_slave.v +// +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: Formal properties for verifying the proper functionality of an +// AXI Stream slave. +// +// Creator: Dan Gisselquist, Ph.D. +// Gisselquist Technology, LLC +// +//////////////////////////////////////////////////////////////////////////////// +// +// Copyright (C) 2019-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 faxis_slave #( + parameter F_MAX_PACKET = 0, + parameter F_MIN_PACKET = 0, + parameter F_MAX_STALL = 0, + parameter C_S_AXI_DATA_WIDTH = 32, + parameter C_S_AXI_ID_WIDTH = 1, + parameter C_S_AXI_ADDR_WIDTH = 1, + parameter C_S_AXI_USER_WIDTH = 1, + parameter [0:0] OPT_ASYNC_RESET = 1'b0, + // + // F_LGDEPTH is the number of bits necessary to represent a packets + // length + parameter F_LGDEPTH = 32, + // + localparam AW = C_S_AXI_ADDR_WIDTH, + localparam DW = C_S_AXI_DATA_WIDTH, + localparam IDW = C_S_AXI_ID_WIDTH, + localparam UW = C_S_AXI_USER_WIDTH + // + ) ( + // + input wire i_aclk, i_aresetn, + input wire i_tvalid, + input wire i_tready = 1, + input wire [DW-1:0] i_tdata, + input wire [DW/8-1:0] i_tstrb = {(DW/8){1'b1}}, + input wire [DW/8-1:0] i_tkeep = {(DW/8){1'b1}}, + input wire i_tlast, + input wire [(IDW>0?IDW:1)-1:0] i_tid = {(IDW){1'b0}}, + input wire [(AW>0?AW:1)-1:0] i_tdest = {(AW){1'b0}}, + input wire [(UW>0?UW:1)-1:0] i_tuser = {(UW){1'b0}}, + // + output reg [F_LGDEPTH-1:0] f_bytecount, + //(* anyconst *) output reg [AW+IDW-1:0] f_routecheck + ); + +`define SLAVE_ASSUME assume +`define SLAVE_ASSERT assert + + localparam F_STALLBITS = (F_MAX_STALL <= 1) + ? 1 : $clog2(F_MAX_STALL+2); + reg f_past_valid; + reg [F_LGDEPTH-1:0] f_vbytes; + reg [F_STALLBITS-1:0] f_stall_count; + integer iB; + genvar k; + + // + // f_past_valid is used to make certain that temporal assertions + // depending upon past values depend upon *valid* past values. + // It is true for all clocks other than the first clock. + initial f_past_valid = 1'b0; + always @(posedge i_aclk) + f_past_valid <= 1'b1; + + // + // Reset should always be active (low) initially + always @(posedge i_aclk) + if (!f_past_valid) + `SLAVE_ASSUME(!i_aresetn); + + // + // During and following a reset, TVALID should be deasserted + always @(posedge i_aclk) + if ((!f_past_valid)||(!i_aresetn && OPT_ASYNC_RESET)||($past(!i_aresetn))) + `SLAVE_ASSUME(!i_tvalid); + + // + // If TVALID but not TREADY, then the master isn't allowed to change + // anything until the slave asserts TREADY. + always @(posedge i_aclk) + if ((f_past_valid)&&($past(i_aresetn))&&(!OPT_ASYNC_RESET || i_aresetn) + &&($past(i_tvalid))&&(!$past(i_tready))) + begin + `SLAVE_ASSUME(i_tvalid); + `SLAVE_ASSUME($stable(i_tstrb)); + `SLAVE_ASSUME($stable(i_tkeep)); + `SLAVE_ASSUME($stable(i_tlast)); + `SLAVE_ASSUME($stable(i_tid)); + `SLAVE_ASSUME($stable(i_tdest)); + `SLAVE_ASSUME($stable(i_tuser)); + end + + generate for(k=0; k<DW/8; k=k+1) + begin : CHECK_PARTIAL_DATA + + // If TVALID && !TREADY, only those TDATA values with TKEEP + // high are required to maintain their values until TREADY + // becomes true. + always @(posedge i_aclk) + if ((f_past_valid)&&($past(i_aresetn)) + &&(!OPT_ASYNC_RESET || i_aresetn) + &&($past(i_tvalid))&&(!$past(i_tready))) + begin + if (i_tkeep[k]) + `SLAVE_ASSUME($stable(i_tdata[k*8 +: 8])); + // else this is a null (don't care) byte, with + // no data within it + // + end + + end endgenerate + + // + // TKEEP == LOW and TSTRB == HIGH is reserved per the spec, and + // must not be used + always @(posedge i_aclk) + if (i_tvalid) + `SLAVE_ASSUME((~i_tkeep & i_tstrb)==0); + + // + // f_vbytes is the number of valid bytes contained in the current beat + // It is used for counting packet lengths below. + always @(*) + if (!i_tvalid) + f_vbytes = 0; + else begin + f_vbytes = 0; + for(iB=0; iB < DW/8; iB=iB+1) + if (i_tkeep[iB] && i_tstrb[iB]) + f_vbytes = f_vbytes + 1; + end + + // + // f_bytecount is the number of bytes that have taken place so far in + // the current packet transmission. Note that we are *only* counting + // our location within the stream if the TUSER and TDEST fields match + // our (solver chosen) ROUTECHECK. That way we don't have to check + // *EVERY POSSIBLE* TUSER and TDEST combination. + initial f_bytecount = 0; + always @(posedge i_aclk) + if (!i_aresetn) + f_bytecount <= 0; + else if (i_tready && i_tvalid /*&& ({ i_tuser, i_tdest } == f_routecheck)*/) + begin + if (i_tlast) + f_bytecount <= 0; + else + f_bytecount <= f_bytecount + f_vbytes; + end + + // + // Count the number of clock cycles between ready's. We'll use this in + // a bit to insist on an (optional) minimum transfer speed. + initial f_stall_count = 0; + always @(posedge i_aclk) + if (!i_aresetn || !i_tvalid || i_tready) + f_stall_count <= 0; + else if (!(&f_stall_count)) + f_stall_count <= f_stall_count + 1; + + // + // F_MAX_PACKET + // + // An optional check, to make certain packets don't exceed some maximum + // length + generate if (F_MAX_PACKET > 0) + begin : MAX_PACKET + + always @(*) + `SLAVE_ASSUME(f_bytecount + f_vbytes <= F_MAX_PACKET); + + end endgenerate + + // + // F_MIN_PACKET + // + // An optoinal check, forcing a minimum packet length + generate if (F_MIN_PACKET > 0) + begin : MIN_PACKET + + always @(*) + if (i_tvalid && i_tlast) + `SLAVE_ASSUME(f_bytecount + f_vbytes >= F_MIN_PACKET); + + end endgenerate + + // + // F_MAX_STALL + // + // Another optional check, this time insisting that the READY flag can + // only be low for up to F_MAX_STALL clocks. + // + generate if (F_MAX_STALL > 0) + begin : MAX_STALL_CHECK + + always @(*) + `SLAVE_ASSERT(f_stall_count < F_MAX_STALL); + + end endgenerate +endmodule +`undef SLAVE_ASSUME +`undef SLAVE_ASSERT + diff --git a/testsuite/ghdl-issues/issue1309/tb_formal_top.v b/testsuite/ghdl-issues/issue1309/tb_formal_top.v new file mode 100644 index 0000000..1bbc87e --- /dev/null +++ b/testsuite/ghdl-issues/issue1309/tb_formal_top.v @@ -0,0 +1,131 @@ +`default_nettype none +module tb_formal_top #( + parameter no_backpressure = 0 +) ( + input wire clk, + input wire aresetn, + + input wire [31:0] s_axis_tdata, + input wire s_axis_tlast, + input wire s_axis_tvalid, + output wire s_axis_tready, + + output wire [31:0] m_axis_tdata, + output wire m_axis_tlast, + output wire m_axis_tvalid, + input wire m_axis_tready, + + output wire signed [31:0] discrepancy +); + + reg [31:0] input_byte_count; + reg [31:0] output_byte_count; + //reg [0+0-1:0] input_routecheck; + //reg [0+0-1:0] output_routecheck; + + reg f_past_valid; + wire signed [31:0] byte_count_discrepancy; + reg packet_end; + +faxis_slave #( + .F_MAX_PACKET(0), + .F_MIN_PACKET(0), + .F_MAX_STALL(0), + .C_S_AXI_DATA_WIDTH(32), + .C_S_AXI_ID_WIDTH(0), + .C_S_AXI_ADDR_WIDTH(0), + .C_S_AXI_USER_WIDTH(0), + .OPT_ASYNC_RESET(1'b0) +) axis_slave_formal_properties ( + .i_aclk(clk), + .i_aresetn(aresetn), + .i_tvalid(s_axis_tvalid), + .i_tready(s_axis_tready), + .i_tdata(s_axis_tdata), + .i_tlast(s_axis_tlast), + .f_bytecount(input_byte_count) + //.f_routecheck(input_routecheck) +); + +faxis_master #( + .F_MAX_PACKET(0), + .F_MIN_PACKET(0), + .F_MAX_STALL(0), + .C_S_AXI_DATA_WIDTH(32), + .C_S_AXI_ID_WIDTH(0), + .C_S_AXI_ADDR_WIDTH(0), + .C_S_AXI_USER_WIDTH(0), + .OPT_ASYNC_RESET(1'b0) +) axis_master_formal_properties ( + .i_aclk(clk), + .i_aresetn(aresetn), + .i_tvalid(m_axis_tvalid), + .i_tready(m_axis_tready), + .i_tdata(m_axis_tdata), + .i_tlast(m_axis_tlast), + .f_bytecount(output_byte_count) + //.f_routecheck(output_routecheck) +); + +axis_squarer axis_dut ( + .clk(clk), + .aresetn(aresetn), + .s_axis_tdata(s_axis_tdata), + .s_axis_tvalid(s_axis_tvalid), + .s_axis_tready(s_axis_tready), + .s_axis_tlast(s_axis_tlast), + .m_axis_tdata(m_axis_tdata), + .m_axis_tvalid(m_axis_tvalid), + .m_axis_tready(m_axis_tready), + .m_axis_tlast(m_axis_tlast) +); + +// f_past_valid is used to make certain that temporal assertions +// depending upon past values depend upon *valid* past values. +// It is true for all clocks other than the first clock. +initial f_past_valid = 1'b0; +always @(posedge clk) + f_past_valid <= 1'b1; + +always @(*) +begin + assert(input_byte_count%4==0); + assert(output_byte_count%4==0); + byte_count_discrepancy = input_byte_count-output_byte_count; + discrepancy <= byte_count_discrepancy; + assume(input_byte_count<=32'h7fffffff); + assert(output_byte_count<=32'h20); + if (aresetn == 1) begin + //assert(byte_count_discrepancy>=-36); + /*assert(byte_count_discrepancy%32 == 0 + || byte_count_discrepancy%32 == 4 + || byte_count_discrepancy%32 == -4);*/ + end + // Hints below are only for the cover property + //assume(aresetn == f_past_valid); + //assume(s_axis_tvalid == 1'b1); + //assume(m_axis_tready == 1'b1); + //assume(input_byte_count & 32'hFFFF0000 == 0); + //cover(byte_count_discrepancy < -4); + //cover(output_byte_count==16); +end + +always @(posedge clk) +begin + if (f_past_valid && $past(aresetn)==1 && aresetn ==1) begin + if ($past(s_axis_tvalid) == 1'b1 && $past(s_axis_tready) == 1'b1) begin + assert(m_axis_tvalid == 1'b1); + assert(~$past(s_axis_tdata)==m_axis_tdata); + end + end + if (no_backpressure==1) begin + assume(m_axis_tready==1); + assume(s_axis_tlast==0); + end + cover(f_past_valid && $past(aresetn)==1 && aresetn==1 + && $past(s_axis_tready)==1'b0 && $past(m_axis_tvalid)==1'b0 + && s_axis_tready==1'b1 && m_axis_tvalid==1'b0); + //cover(output_byte_count==16'h10); +end + +endmodule diff --git a/testsuite/ghdl-issues/issue1309/testsuite.sh b/testsuite/ghdl-issues/issue1309/testsuite.sh new file mode 100755 index 0000000..a50cfc8 --- /dev/null +++ b/testsuite/ghdl-issues/issue1309/testsuite.sh @@ -0,0 +1,10 @@ +#!/bin/sh + +topdir=../.. +. $topdir/testenv.sh + +#formal axis_squarer +run_symbiyosys axis_squarer.sby cover + +clean +echo OK |