Add test from ghdl/ghdl#1309

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