Add simple formal bus properties check

sourceme

@@ -1,3 +1,4 @@
 export PATH="$PATH:$PWD/scripts"
 export PROJ_ROOT=$PWD
 export HDL=$PROJ_ROOT/hdl
+export SCRIPTS=$PROJ_ROOT/scripts

test/formal/.gitignore

@@ -0,0 +1,2 @@
+*.log
+*.smt2

test/formal/bus_compliance_2port/Makefile

@@ -0,0 +1,5 @@
+DOTF=tb.f
+TOP=tb
+YOSYS_SMT_SOLVER=boolector
+
+include $(SCRIPTS)/formal.mk

test/formal/bus_compliance_2port/tb.f

@@ -0,0 +1,4 @@
+file tb.v
+file ../common/ahbl_slave_assumptions.v
+file ../common/ahbl_master_assertions.v
+list $HDL/hazard3.f

test/formal/bus_compliance_2port/tb.v

@@ -0,0 +1,152 @@
+// Assume bus responses to both ports are well-formed, assert that bus
+// requests are well-formed.
+
+module tb;
+
+reg clk;
+reg rst_n = 1'b0;
+always @ (posedge clk)
+	rst_n <= 1'b1;
+
+// ----------------------------------------------------------------------------
+// DUT
+
+(* keep *) wire [31:0]  i_haddr;
+(* keep *) wire         i_hwrite;
+(* keep *) wire [1:0]   i_htrans;
+(* keep *) wire [2:0]   i_hsize;
+(* keep *) wire [2:0]   i_hburst;
+(* keep *) wire [3:0]   i_hprot;
+(* keep *) wire         i_hmastlock;
+(* keep *) wire         i_hready;
+(* keep *) wire         i_hresp;
+(* keep *) wire [31:0]  i_hwdata;
+(* keep *) wire [31:0]  i_hrdata;
+
+(* keep *) wire [31:0]  d_haddr;
+(* keep *) wire         d_hwrite;
+(* keep *) wire [1:0]   d_htrans;
+(* keep *) wire [2:0]   d_hsize;
+(* keep *) wire [2:0]   d_hburst;
+(* keep *) wire [3:0]   d_hprot;
+(* keep *) wire         d_hmastlock;
+(* keep *) wire         d_hready;
+(* keep *) wire         d_hresp;
+(* keep *) wire [31:0]  d_hwdata;
+(* keep *) wire [31:0]  d_hrdata;
+
+(* keep *) reg  [15:0]  irq;
+
+hazard3_cpu_2port dut (
+	.clk          (clk),
+	.rst_n        (rst_n),
+
+	.i_haddr      (i_haddr),
+	.i_hwrite     (i_hwrite),
+	.i_htrans     (i_htrans),
+	.i_hsize      (i_hsize),
+	.i_hburst     (i_hburst),
+	.i_hprot      (i_hprot),
+	.i_hmastlock  (i_hmastlock),
+	.i_hready     (i_hready),
+	.i_hresp      (i_hresp),
+	.i_hwdata     (i_hwdata),
+	.i_hrdata     (i_hrdata),
+
+	.d_haddr      (d_haddr),
+	.d_hwrite     (d_hwrite),
+	.d_htrans     (d_htrans),
+	.d_hsize      (d_hsize),
+	.d_hburst     (d_hburst),
+	.d_hprot      (d_hprot),
+	.d_hmastlock  (d_hmastlock),
+	.d_hready     (d_hready),
+	.d_hresp      (d_hresp),
+	.d_hwdata     (d_hwdata),
+	.d_hrdata     (d_hrdata),
+
+	.irq          (irq)
+);
+
+// ----------------------------------------------------------------------------
+// Bus properties
+
+// -1 -> unconstrained, >=0 -> max length
+localparam MAX_BUS_STALL = -1;
+
+ahbl_slave_assumptions #(
+	.MAX_BUS_STALL (MAX_BUS_STALL)
+) i_assumptions (
+	.clk             (clk),
+	.rst_n           (rst_n),
+
+	.dst_hready_resp (i_hready),
+	.dst_hready      (i_hready),
+	.dst_hresp       (i_hresp),
+	.dst_haddr       (i_haddr),
+	.dst_hwrite      (i_hwrite),
+	.dst_htrans      (i_htrans),
+	.dst_hsize       (i_hsize),
+	.dst_hburst      (i_hburst),
+	.dst_hprot       (i_hprot),
+	.dst_hmastlock   (i_hmastlock),
+	.dst_hwdata      (i_hwdata),
+	.dst_hrdata      (i_hrdata)
+);
+
+ahbl_slave_assumptions #(
+	.MAX_BUS_STALL (MAX_BUS_STALL)
+) d_assumptions (
+	.clk             (clk),
+	.rst_n           (rst_n),
+
+	.dst_hready_resp (d_hready),
+	.dst_hready      (d_hready),
+	.dst_hresp       (d_hresp),
+	.dst_haddr       (d_haddr),
+	.dst_hwrite      (d_hwrite),
+	.dst_htrans      (d_htrans),
+	.dst_hsize       (d_hsize),
+	.dst_hburst      (d_hburst),
+	.dst_hprot       (d_hprot),
+	.dst_hmastlock   (d_hmastlock),
+	.dst_hwdata      (d_hwdata),
+	.dst_hrdata      (d_hrdata)
+);
+
+ahbl_master_assertions i_assertions (
+	.clk             (clk),
+	.rst_n           (rst_n),
+
+	.src_hready      (i_hready),
+	.src_hresp       (i_hresp),
+	.src_haddr       (i_haddr),
+	.src_hwrite      (i_hwrite),
+	.src_htrans      (i_htrans),
+	.src_hsize       (i_hsize),
+	.src_hburst      (i_hburst),
+	.src_hprot       (i_hprot),
+	.src_hmastlock   (i_hmastlock),
+	.src_hwdata      (i_hwdata),
+	.src_hrdata      (i_hrdata)
+);
+
+
+ahbl_master_assertions d_assertions (
+	.clk             (clk),
+	.rst_n           (rst_n),
+
+	.src_hready      (d_hready),
+	.src_hresp       (d_hresp),
+	.src_haddr       (d_haddr),
+	.src_hwrite      (d_hwrite),
+	.src_htrans      (d_htrans),
+	.src_hsize       (d_hsize),
+	.src_hburst      (d_hburst),
+	.src_hprot       (d_hprot),
+	.src_hmastlock   (d_hmastlock),
+	.src_hwdata      (d_hwdata),
+	.src_hrdata      (d_hrdata)
+);
+
+endmodule

test/formal/common/ahbl_master_assertions.v

@@ -24,10 +24,8 @@ module ahbl_master_assertions #(
 	input wire               clk,
 	input wire               rst_n,
 
-	// Upstream AHB-Lite slave port
-	output wire               src_hready_resp,
 	input wire               src_hready,
-	output wire               src_hresp,
+	input wire               src_hresp,
 	input wire [W_ADDR-1:0]  src_haddr,
 	input wire               src_hwrite,
 	input wire [1:0]         src_htrans,
@@ -36,7 +34,7 @@ module ahbl_master_assertions #(
 	input wire [3:0]         src_hprot,
 	input wire               src_hmastlock,
 	input wire [W_DATA-1:0]  src_hwdata,
-	output wire [W_DATA-1:0]  src_hrdata
+	input wire [W_DATA-1:0]  src_hrdata
 );
 
 // Data-phase monitoring 

test/formal/common/ahbl_slave_assumptions.v

@@ -25,18 +25,17 @@ module ahbl_slave_assumptions #(
 	input wire               clk,
 	input wire               rst_n,
 
-	// Downstream AHB-Lite master port
 	input wire               dst_hready_resp,
-	output wire               dst_hready,
+	input wire               dst_hready,
 	input wire               dst_hresp,
-	output wire [W_ADDR-1:0]  dst_haddr,
+	input wire [W_ADDR-1:0]  dst_haddr,
-	output wire               dst_hwrite,
+	input wire               dst_hwrite,
-	output wire [1:0]         dst_htrans,
+	input wire [1:0]         dst_htrans,
-	output wire [2:0]         dst_hsize,
+	input wire [2:0]         dst_hsize,
-	output wire [2:0]         dst_hburst,
+	input wire [2:0]         dst_hburst,
-	output wire [3:0]         dst_hprot,
+	input wire [3:0]         dst_hprot,
-	output wire               dst_hmastlock,
+	input wire               dst_hmastlock,
-	output wire [W_DATA-1:0]  dst_hwdata,
+	input wire [W_DATA-1:0]  dst_hwdata,
 	input wire [W_DATA-1:0]  dst_hrdata
 );