axipc.v

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.v,v
//  File Revision       : 1.157
//
//  Release Information : BP062-VL-70002-r0p0-00rel0
//
//------------------------------------------------------------------------------
//  Purpose             : This is the AXI Protocol Checker using OVL
//
//                        Supports bus widths of 32, 64, 128, 256, 512, 1024 bit
//                        Parameterisable write interleave depth
//                        Supports a single outstanding exclusive read per ID
//============================================================================--

//----------------------------------------------------------------------------
// CONTENTS
// ========
//  282.  Module: AxiPC
//  349.    1) Parameters
//  353.         - Configurable (user can set)
//  402.         - Calculated (user should not override)
//  466.    2) Inputs (no outputs)
//  470.         - Global Signals
//  476.         - Write Address Channel
//  491.         - Write Data Channel
//  502.         - Write Response Channel
//  511.         - Read Address Channel
//  526.         - Read Data Channel
//  536.         - Low Power Interface
//  544.    3) Wire and Reg Declarations
//  643.    4) Verilog Defines
//  647.         - Lock FSM States
//  656.         - Clock and Reset
//  688.         - OVL Version Specific Macros
//  730.    5) Initialize simulation
//  735.         - Format for time reporting
//  741.         - Indicate version of AxiPC
//  746.         - Warn if any/some recommended rules are disabled
//  756.         - Warn if any/some channel rules are ignored
//  772. 
//  773.  AXI Rules: Write Address Channel (*_AW*)
//  778.    1) Functional Rules
//  782.         - AXI_ERRM_AWADDR_BOUNDARY
//  806.         - AXI_ERRM_AWADDR_WRAP_ALIGN
//  818.         - AXI_ERRM_AWBURST
//  830.         - AXI_ERRM_AWCACHE
//  842.         - AXI_ERRM_AWLEN_WRAP
//  857.         - AXI_ERRM_AWLOCK
//  869.         - AXI_ERRM_AWLOCK_END
//  885.         - AXI_ERRM_AWLOCK_ID
//  899.         - AXI_ERRM_AWLOCK_LAST
//  913.         - AXI_ERRM_AWLOCK_START
//  929.         - AXI_ERRM_AWSIZE
//  943.         - AXI_ERRM_AWVALID_RESET
//  955.         - AXI_RECM_AWLOCK_BOUNDARY
//  971.         - AXI_RECM_AWLOCK_CTRL 
//  986.         - AXI_RECM_AWLOCK_NUM
// 1002.    2) Handshake Rules
// 1006.         - AXI_ERRM_AWADDR_STABLE
// 1019.         - AXI_ERRM_AWBURST_STABLE
// 1032.         - AXI_ERRM_AWCACHE_STABLE
// 1045.         - AXI_ERRM_AWID_STABLE
// 1058.         - AXI_ERRM_AWLEN_STABLE
// 1071.         - AXI_ERRM_AWLOCK_STABLE
// 1084.         - AXI_ERRM_AWPROT_STABLE
// 1097.         - AXI_ERRM_AWSIZE_STABLE
// 1110.         - AXI_ERRM_AWVALID_STABLE
// 1122.         - AXI_RECS_AWREADY_MAX_WAIT
// 1138.    3) X-Propagation Rules
// 1144.         - AXI_ERRM_AWADDR_X
// 1155.         - AXI_ERRM_AWBURST_X
// 1166.         - AXI_ERRM_AWCACHE_X
// 1177.         - AXI_ERRM_AWID_X
// 1188.         - AXI_ERRM_AWLEN_X
// 1199.         - AXI_ERRM_AWLOCK_X
// 1210.         - AXI_ERRM_AWPROT_X
// 1221.         - AXI_ERRM_AWSIZE_X
// 1232.         - AXI_ERRM_AWVALID_X
// 1243.         - AXI_ERRS_AWREADY_X
// 1257. 
// 1258.  AXI Rules: Write Data Channel (*_W*)
// 1263.    1) Functional Rules
// 1267.         - AXI_ERRM_WDATA_NUM
// 1282.         - AXI_ERRM_WDATA_ORDER
// 1293.         - AXI_ERRM_WDEPTH
// 1305.         - AXI_ERRM_WSTRB
// 1316.         - AXI_ERRM_WVALID_RESET
// 1329.    2) Handshake Rules
// 1333.         - AXI_ERRM_WDATA_STABLE
// 1346.         - AXI_ERRM_WID_STABLE
// 1359.         - AXI_ERRM_WLAST_STABLE
// 1372.         - AXI_ERRM_WSTRB_STABLE
// 1385.         - AXI_ERRM_WVALID_STABLE
// 1397.         - AXI_RECS_WREADY_MAX_WAIT 
// 1413.    3) X-Propagation Rules
// 1419.         - AXI_ERRM_WDATA_X
// 1430.         - AXI_ERRM_WID_X
// 1441.         - AXI_ERRM_WLAST_X
// 1452.         - AXI_ERRM_WSTRB_X
// 1463.         - AXI_ERRM_WVALID_X
// 1474.         - AXI_ERRS_WREADY_X
// 1488. 
// 1489.  AXI Rules: Write Response Channel (*_B*)
// 1494.    1) Functional Rules
// 1498.         - AXI_ERRS_BRESP
// 1509.         - AXI_ERRS_BRESP_ALL_DONE_EOS
// 1526.         - AXI_ERRS_BRESP_EXOKAY
// 1537.         - AXI_ERRS_BVALID_RESET
// 1550.    2) Handshake Rules
// 1554.         - AXI_ERRS_BID_STABLE
// 1567.         - AXI_ERRS_BRESP_STABLE
// 1580.         - AXI_ERRS_BVALID_STABLE
// 1592.         - AXI_RECM_BREADY_MAX_WAIT 
// 1608.    3) X-Propagation Rules
// 1614.         - AXI_ERRM_BREADY_X
// 1625.         - AXI_ERRS_BID_X
// 1636.         - AXI_ERRS_BRESP_X
// 1647.         - AXI_ERRS_BVALID_X
// 1661. 
// 1662.  AXI Rules: Read Address Channel (*_AR*)
// 1667.    1) Functional Rules
// 1671.         - AXI_ERRM_ARADDR_BOUNDARY
// 1695.         - AXI_ERRM_ARADDR_WRAP_ALIGN
// 1707.         - AXI_ERRM_ARBURST
// 1719.         - AXI_ERRM_ARCACHE
// 1731.         - AXI_ERRM_ARLEN_WRAP
// 1746.         - AXI_ERRM_ARLOCK
// 1758.         - AXI_ERRM_ARLOCK_END
// 1774.         - AXI_ERRM_ARLOCK_ID
// 1788.         - AXI_ERRM_ARLOCK_LAST
// 1802.         - AXI_ERRM_ARLOCK_START
// 1818.         - AXI_ERRM_ARSIZE
// 1830.         - AXI_ERRM_ARVALID_RESET
// 1842.         - AXI_RECM_ARLOCK_BOUNDARY
// 1858.         - AXI_RECM_ARLOCK_CTRL
// 1873.         - AXI_RECM_ARLOCK_NUM
// 1889.    2) Handshake Rules
// 1893.         - AXI_ERRM_ARADDR_STABLE
// 1906.         - AXI_ERRM_ARBURST_STABLE
// 1919.         - AXI_ERRM_ARCACHE_STABLE
// 1932.         - AXI_ERRM_ARID_STABLE
// 1945.         - AXI_ERRM_ARLEN_STABLE
// 1958.         - AXI_ERRM_ARLOCK_STABLE
// 1971.         - AXI_ERRM_ARPROT_STABLE
// 1984.         - AXI_ERRM_ARSIZE_STABLE
// 1997.         - AXI_ERRM_ARVALID_STABLE
// 2009.         - AXI_RECS_ARREADY_MAX_WAIT 
// 2025.    3) X-Propagation Rules
// 2031.         - AXI_ERRM_ARADDR_X
// 2042.         - AXI_ERRM_ARBURST_X
// 2053.         - AXI_ERRM_ARCACHE_X
// 2064.         - AXI_ERRM_ARID_X
// 2075.         - AXI_ERRM_ARLEN_X
// 2086.         - AXI_ERRM_ARLOCK_X
// 2097.         - AXI_ERRM_ARPROT_X
// 2108.         - AXI_ERRM_ARSIZE_X
// 2119.         - AXI_ERRM_ARVALID_X
// 2130.         - AXI_ERRS_ARREADY_X
// 2144. 
// 2145.  AXI Rules: Read Data Channel (*_R*)
// 2150.    1) Functional Rules
// 2154.         - AXI_ERRS_RDATA_NUM
// 2168.         - AXI_ERRS_RLAST_ALL_DONE_EOS
// 2185.         - AXI_ERRS_RID
// 2198.         - AXI_ERRS_RRESP_EXOKAY
// 2210.         - AXI_ERRS_RVALID_RESET
// 2223.    2) Handshake Rules
// 2227.         - AXI_ERRS_RDATA_STABLE
// 2240.         - AXI_ERRS_RID_STABLE
// 2253.         - AXI_ERRS_RLAST_STABLE
// 2266.         - AXI_ERRS_RRESP_STABLE
// 2279.         - AXI_ERRS_RVALID_STABLE
// 2291.         - AXI_RECM_RREADY_MAX_WAIT 
// 2307.    3) X-Propagation Rules
// 2313.         - AXI_ERRM_RREADY_X
// 2324.         - AXI_ERRS_RID_X
// 2335.         - AXI_ERRS_RLAST_X
// 2346.         - AXI_ERRS_RRESP_X
// 2357.         - AXI_ERRS_RVALID_X
// 2371. 
// 2372.  AXI Rules: Low Power Interface (*_C*)
// 2377.    1) Functional Rules (none for Low Power signals)
// 2382.    2) Handshake Rules (asynchronous to ACLK)
// 2389.         - AXI_ERRL_CSYSACK_FALL
// 2400.         - AXI_ERRL_CSYSACK_RISE
// 2411.         - AXI_ERRL_CSYSREQ_FALL
// 2422.         - AXI_ERRL_CSYSREQ_RISE
// 2434.    3) X-Propagation Rules
// 2440.         - AXI_ERRL_CACTIVE_X
// 2451.         - AXI_ERRL_CSYSACK_X
// 2462.         - AXI_ERRL_CSYSREQ_X
// 2476. 
// 2477.  AXI Rules: Exclusive Access
// 2485.    1) Functional Rules
// 2487.         -
// 2490.         - AXI_ERRM_EXCL_ALIGN
// 2511.         - AXI_ERRM_EXCL_LEN
// 2529.         - AXI_RECM_EXCL_MATCH
// 2551.         - AXI_ERRM_EXCL_MAX
// 2572.         - AXI_RECM_EXCL_PAIR
// 2587. 
// 2588.  AXI Rules: USER_* Rules (extension to AXI)
// 2596.    1) Functional Rules (none for USER signals)
// 2601.    2) Handshake Rules
// 2605.         - AXI_ERRM_AWUSER_STABLE
// 2618.         - AXI_ERRM_WUSER_STABLE
// 2631.         - AXI_ERRS_BUSER_STABLE
// 2644.         - AXI_ERRM_ARUSER_STABLE
// 2657.         - AXI_ERRS_RUSER_STABLE
// 2671.    3) X-Propagation Rules
// 2677.         - AXI_ERRM_AWUSER_X
// 2688.         - AXI_ERRM_WUSER_X
// 2699.         - AXI_ERRS_BUSER_X
// 2710.         - AXI_ERRM_ARUSER_X
// 2721.         - AXI_ERRS_RUSER_X
// 2735. 
// 2736.  Auxiliary Logic
// 2741.    1) Rules for Auxiliary Logic
// 2746.       a) Master (AUXM*)
// 2750.         - AXI_AUXM_DATA_WIDTH
// 2765.         - AXI_AUXM_RCAM_OVERFLOW
// 2776.         - AXI_AUXM_RCAM_UNDERFLOW
// 2787.         - AXI_AUXM_WCAM_OVERFLOW
// 2798.         - AXI_AUXM_WCAM_UNDERFLOW
// 2810.    2) Combinatorial Logic
// 2815.       a) Masks
// 2819.            - AlignMaskR
// 2841.            - AlignMaskW
// 2863.            - ExclMask
// 2871.            - WdataMask
// 2885.       b) Increments
// 2889.            - ArAddrIncr
// 2897.            - AwAddrIncr
// 2906.       c) Conversions
// 2910.            - ArLenInBytes
// 2918.            - ArSizeInBits
// 2926.            - AwSizeInBits
// 2935.       d) Other
// 2939.            - ArExclPending
// 2945.            - ArLenPending
// 2952.    3) EXCL & LOCK Accesses
// 2956.         - Exclusive Access Storage
// 3004.         - Lock State Machine
// 3047.         - Lock Storage
// 3070.         - Lock Arrays
// 3138.    4) Content addressable memories (CAMs)
// 3142.         - Read CAMSs (CAM+Shift)
// 3249.         - Write CAMs (CAM+Shift)
// 3545.         - Write Depth array
// 3584.    5) Verilog Functions
// 3588.         - CheckBurst
// 3687.         - CheckStrb
// 3725.         - CheckXorZ
// 3742.         - CheckXorZifValid
// 3764. 
// 3765.  End of File
// 3770.    1) Clear Verilog Defines
// 3797.    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,