axipc.sv

amba3 sva 完全验证的代码

//============================================================================--
//  This confidential and proprietary software may be used only as
//  authorised by a licensing agreement from ARM Limited
//    (C) COPYRIGHT 2003-2006 ARM Limited
//        ALL RIGHTS RESERVED
//  The entire notice above must be reproduced on all authorised
//  copies and copies may only be made to the extent permitted
//  by a licensing agreement from ARM Limited.
//
//
//------------------------------------------------------------------------------
//  Version and Release Control Information:
//
//  File Name           : AxiPC.sv,v
//  File Revision       : 1.9
//
//  Release Information : BP062-VL-70004-r0p0-00rel0
//
//------------------------------------------------------------------------------
//  Purpose             : This is the AXI Protocol Checker using SVA
//
//                        Supports bus widths of 32, 64, 128, 256, 512, 1024 bit
//                        Parameterisable write interleave depth
//                        Supports a single outstanding exclusive read per ID
//============================================================================--

//----------------------------------------------------------------------------
// CONTENTS
// ========
//  279.  Module: AxiPC
//  346.    1) Parameters
//  350.         - Configurable (user can set)
//  399.         - Calculated (user should not override)
//  463.    2) Inputs (no outputs)
//  467.         - Global Signals
//  473.         - Write Address Channel
//  488.         - Write Data Channel
//  499.         - Write Response Channel
//  508.         - Read Address Channel
//  523.         - Read Data Channel
//  533.         - Low Power Interface
//  541.    3) Wire and Reg Declarations
//  640.    4) Verilog Defines
//  644.         - Lock FSM States
//  653.         - Clock and Reset
//  686.    5) Initialize simulation
//  691.         - Format for time reporting
//  697.         - Indicate version of AxiPC
//  702.         - Warn if any/some recommended rules are disabled
//  712.         - Warn if any/some channel rules are ignored
//  728. 
//  729.  AXI Rules: Write Address Channel (*_AW*)
//  734.    1) Functional Rules
//  738.         - AXI_ERRM_AWADDR_BOUNDARY
//  762.         - AXI_ERRM_AWADDR_WRAP_ALIGN
//  774.         - AXI_ERRM_AWBURST
//  786.         - AXI_ERRM_AWCACHE
//  798.         - AXI_ERRM_AWLEN_WRAP
//  813.         - AXI_ERRM_AWLOCK
//  825.         - AXI_ERRM_AWLOCK_END
//  841.         - AXI_ERRM_AWLOCK_ID
//  855.         - AXI_ERRM_AWLOCK_LAST
//  869.         - AXI_ERRM_AWLOCK_START
//  885.         - AXI_ERRM_AWSIZE
//  899.         - AXI_ERRM_AWVALID_RESET
//  911.         - AXI_RECM_AWLOCK_BOUNDARY
//  927.         - AXI_RECM_AWLOCK_CTRL 
//  942.         - AXI_RECM_AWLOCK_NUM
//  958.    2) Handshake Rules
//  962.         - AXI_ERRM_AWADDR_STABLE
//  975.         - AXI_ERRM_AWBURST_STABLE
//  988.         - AXI_ERRM_AWCACHE_STABLE
// 1001.         - AXI_ERRM_AWID_STABLE
// 1014.         - AXI_ERRM_AWLEN_STABLE
// 1027.         - AXI_ERRM_AWLOCK_STABLE
// 1040.         - AXI_ERRM_AWPROT_STABLE
// 1053.         - AXI_ERRM_AWSIZE_STABLE
// 1066.         - AXI_ERRM_AWVALID_STABLE
// 1078.         - AXI_RECS_AWREADY_MAX_WAIT
// 1094.    3) X-Propagation Rules
// 1100.         - AXI_ERRM_AWADDR_X
// 1111.         - AXI_ERRM_AWBURST_X
// 1122.         - AXI_ERRM_AWCACHE_X
// 1133.         - AXI_ERRM_AWID_X
// 1144.         - AXI_ERRM_AWLEN_X
// 1155.         - AXI_ERRM_AWLOCK_X
// 1166.         - AXI_ERRM_AWPROT_X
// 1177.         - AXI_ERRM_AWSIZE_X
// 1188.         - AXI_ERRM_AWVALID_X
// 1199.         - AXI_ERRS_AWREADY_X
// 1213. 
// 1214.  AXI Rules: Write Data Channel (*_W*)
// 1219.    1) Functional Rules
// 1223.         - AXI_ERRM_WDATA_NUM
// 1238.         - AXI_ERRM_WDATA_ORDER
// 1249.         - AXI_ERRM_WDEPTH
// 1261.         - AXI_ERRM_WSTRB
// 1272.         - AXI_ERRM_WVALID_RESET
// 1285.    2) Handshake Rules
// 1289.         - AXI_ERRM_WDATA_STABLE
// 1302.         - AXI_ERRM_WID_STABLE
// 1315.         - AXI_ERRM_WLAST_STABLE
// 1328.         - AXI_ERRM_WSTRB_STABLE
// 1341.         - AXI_ERRM_WVALID_STABLE
// 1353.         - AXI_RECS_WREADY_MAX_WAIT 
// 1369.    3) X-Propagation Rules
// 1375.         - AXI_ERRM_WDATA_X
// 1386.         - AXI_ERRM_WID_X
// 1397.         - AXI_ERRM_WLAST_X
// 1408.         - AXI_ERRM_WSTRB_X
// 1419.         - AXI_ERRM_WVALID_X
// 1430.         - AXI_ERRS_WREADY_X
// 1444. 
// 1445.  AXI Rules: Write Response Channel (*_B*)
// 1450.    1) Functional Rules
// 1454.         - AXI_ERRS_BRESP
// 1465.         - AXI_ERRS_BRESP_ALL_DONE_EOS
// 1482.         - AXI_ERRS_BRESP_EXOKAY
// 1493.         - AXI_ERRS_BVALID_RESET
// 1506.    2) Handshake Rules
// 1510.         - AXI_ERRS_BID_STABLE
// 1523.         - AXI_ERRS_BRESP_STABLE
// 1536.         - AXI_ERRS_BVALID_STABLE
// 1548.         - AXI_RECM_BREADY_MAX_WAIT 
// 1564.    3) X-Propagation Rules
// 1570.         - AXI_ERRM_BREADY_X
// 1581.         - AXI_ERRS_BID_X
// 1592.         - AXI_ERRS_BRESP_X
// 1603.         - AXI_ERRS_BVALID_X
// 1617. 
// 1618.  AXI Rules: Read Address Channel (*_AR*)
// 1623.    1) Functional Rules
// 1627.         - AXI_ERRM_ARADDR_BOUNDARY
// 1651.         - AXI_ERRM_ARADDR_WRAP_ALIGN
// 1663.         - AXI_ERRM_ARBURST
// 1675.         - AXI_ERRM_ARCACHE
// 1687.         - AXI_ERRM_ARLEN_WRAP
// 1702.         - AXI_ERRM_ARLOCK
// 1714.         - AXI_ERRM_ARLOCK_END
// 1730.         - AXI_ERRM_ARLOCK_ID
// 1744.         - AXI_ERRM_ARLOCK_LAST
// 1758.         - AXI_ERRM_ARLOCK_START
// 1774.         - AXI_ERRM_ARSIZE
// 1786.         - AXI_ERRM_ARVALID_RESET
// 1798.         - AXI_RECM_ARLOCK_BOUNDARY
// 1814.         - AXI_RECM_ARLOCK_CTRL
// 1829.         - AXI_RECM_ARLOCK_NUM
// 1845.    2) Handshake Rules
// 1849.         - AXI_ERRM_ARADDR_STABLE
// 1862.         - AXI_ERRM_ARBURST_STABLE
// 1875.         - AXI_ERRM_ARCACHE_STABLE
// 1888.         - AXI_ERRM_ARID_STABLE
// 1901.         - AXI_ERRM_ARLEN_STABLE
// 1914.         - AXI_ERRM_ARLOCK_STABLE
// 1927.         - AXI_ERRM_ARPROT_STABLE
// 1940.         - AXI_ERRM_ARSIZE_STABLE
// 1953.         - AXI_ERRM_ARVALID_STABLE
// 1965.         - AXI_RECS_ARREADY_MAX_WAIT 
// 1981.    3) X-Propagation Rules
// 1987.         - AXI_ERRM_ARADDR_X
// 1998.         - AXI_ERRM_ARBURST_X
// 2009.         - AXI_ERRM_ARCACHE_X
// 2020.         - AXI_ERRM_ARID_X
// 2031.         - AXI_ERRM_ARLEN_X
// 2042.         - AXI_ERRM_ARLOCK_X
// 2053.         - AXI_ERRM_ARPROT_X
// 2064.         - AXI_ERRM_ARSIZE_X
// 2075.         - AXI_ERRM_ARVALID_X
// 2086.         - AXI_ERRS_ARREADY_X
// 2100. 
// 2101.  AXI Rules: Read Data Channel (*_R*)
// 2106.    1) Functional Rules
// 2110.         - AXI_ERRS_RDATA_NUM
// 2124.         - AXI_ERRS_RLAST_ALL_DONE_EOS
// 2141.         - AXI_ERRS_RID
// 2154.         - AXI_ERRS_RRESP_EXOKAY
// 2166.         - AXI_ERRS_RVALID_RESET
// 2179.    2) Handshake Rules
// 2183.         - AXI_ERRS_RDATA_STABLE
// 2196.         - AXI_ERRS_RID_STABLE
// 2209.         - AXI_ERRS_RLAST_STABLE
// 2222.         - AXI_ERRS_RRESP_STABLE
// 2235.         - AXI_ERRS_RVALID_STABLE
// 2247.         - AXI_RECM_RREADY_MAX_WAIT 
// 2263.    3) X-Propagation Rules
// 2269.         - AXI_ERRM_RREADY_X
// 2280.         - AXI_ERRS_RID_X
// 2291.         - AXI_ERRS_RLAST_X
// 2302.         - AXI_ERRS_RRESP_X
// 2313.         - AXI_ERRS_RVALID_X
// 2327. 
// 2328.  AXI Rules: Low Power Interface (*_C*)
// 2333.    1) Functional Rules (none for Low Power signals)
// 2338.    2) Handshake Rules (asynchronous to ACLK)
// 2345.         - AXI_ERRL_CSYSACK_FALL
// 2356.         - AXI_ERRL_CSYSACK_RISE
// 2367.         - AXI_ERRL_CSYSREQ_FALL
// 2378.         - AXI_ERRL_CSYSREQ_RISE
// 2390.    3) X-Propagation Rules
// 2396.         - AXI_ERRL_CACTIVE_X
// 2407.         - AXI_ERRL_CSYSACK_X
// 2418.         - AXI_ERRL_CSYSREQ_X
// 2432. 
// 2433.  AXI Rules: Exclusive Access
// 2441.    1) Functional Rules
// 2443.         -
// 2446.         - AXI_ERRM_EXCL_ALIGN
// 2467.         - AXI_ERRM_EXCL_LEN
// 2485.         - AXI_RECM_EXCL_MATCH
// 2507.         - AXI_ERRM_EXCL_MAX
// 2528.         - AXI_RECM_EXCL_PAIR
// 2543. 
// 2544.  AXI Rules: USER_* Rules (extension to AXI)
// 2552.    1) Functional Rules (none for USER signals)
// 2557.    2) Handshake Rules
// 2561.         - AXI_ERRM_AWUSER_STABLE
// 2574.         - AXI_ERRM_WUSER_STABLE
// 2587.         - AXI_ERRS_BUSER_STABLE
// 2600.         - AXI_ERRM_ARUSER_STABLE
// 2613.         - AXI_ERRS_RUSER_STABLE
// 2627.    3) X-Propagation Rules
// 2633.         - AXI_ERRM_AWUSER_X
// 2644.         - AXI_ERRM_WUSER_X
// 2655.         - AXI_ERRS_BUSER_X
// 2666.         - AXI_ERRM_ARUSER_X
// 2677.         - AXI_ERRS_RUSER_X
// 2691. 
// 2692.  Auxiliary Logic
// 2697.    1) Rules for Auxiliary Logic
// 2702.       a) Master (AUXM*)
// 2706.         - AXI_AUXM_DATA_WIDTH
// 2721.         - AXI_AUXM_RCAM_OVERFLOW
// 2732.         - AXI_AUXM_RCAM_UNDERFLOW
// 2743.         - AXI_AUXM_WCAM_OVERFLOW
// 2754.         - AXI_AUXM_WCAM_UNDERFLOW
// 2766.    2) Combinatorial Logic
// 2771.       a) Masks
// 2775.            - AlignMaskR
// 2797.            - AlignMaskW
// 2819.            - ExclMask
// 2827.            - WdataMask
// 2841.       b) Increments
// 2845.            - ArAddrIncr
// 2853.            - AwAddrIncr
// 2862.       c) Conversions
// 2866.            - ArLenInBytes
// 2874.            - ArSizeInBits
// 2882.            - AwSizeInBits
// 2891.       d) Other
// 2895.            - ArExclPending
// 2901.            - ArLenPending
// 2908.    3) EXCL & LOCK Accesses
// 2912.         - Exclusive Access Storage
// 2960.         - Lock State Machine
// 3003.         - Lock Storage
// 3026.         - Lock Arrays
// 3094.    4) Content addressable memories (CAMs)
// 3098.         - Read CAMSs (CAM+Shift)
// 3205.         - Write CAMs (CAM+Shift)
// 3501.         - Write Depth array
// 3540.    5) Verilog Functions
// 3544.         - CheckBurst
// 3643.         - CheckStrb
// 3682. 
// 3683.  End of File
// 3688.    1) Clear Verilog Defines
// 3710.    2) End of module
//----------------------------------------------------------------------------

`timescale 1ns/1ns

//------------------------------------------------------------------------------
// AXI Standard Defines
//------------------------------------------------------------------------------
`include "Axi.v"


//------------------------------------------------------------------------------
// INDEX: Module: AxiPC
//------------------------------------------------------------------------------
module AxiPC
  (
   // Global Signals
   ACLK,
   ARESETn,

   // Write Address Channel
   AWID,
   AWADDR,
   AWLEN,
   AWSIZE,
   AWBURST,
   AWLOCK,
   AWCACHE,
   AWPROT,
   AWUSER,
   AWVALID,
   AWREADY,

   // Write Channel
   WID,
   WLAST,
   WDATA,
   WSTRB,
   WUSER,
   WVALID,
   WREADY,

   // Write Response Channel
   BID,
   BRESP,
   BUSER,
   BVALID,
   BREADY,

   // Read Address Channel
   ARID,
   ARADDR,
   ARLEN,
   ARSIZE,
   ARBURST,
   ARLOCK,
   ARCACHE,
   ARPROT,
   ARUSER,
   ARVALID,
   ARREADY,

   // Read Channel
   RID,
   RLAST,
   RDATA,
   RRESP,
   RUSER,
   RVALID,
   RREADY,

   // Low power interface