Giter Site home page Giter Site logo

zipcpu / wb2axip Goto Github PK

View Code? Open in Web Editor NEW
437.0 30.0 92.0 9.18 MB

Bus bridges and other odds and ends

Verilog 93.53% Makefile 2.70% C++ 1.58% VHDL 1.08% Shell 0.22% SystemVerilog 0.89%
fpga wishbone wishbone-bus axi-bus xilinx xilinx-vivado gplv3

wb2axip's Introduction

WB2AXIP: Bus interconnects, bridges, and other components

The bus components and bridges within this repository are unique in that they are all designed for 100% throughput with no throughput overhead. They are also unique in that the vast majority of the cores within have all been formally verified.

Where the protocol allows it, such as with AXI4, AXI-lite, and Wishbone B4 pipelined, multiple transactions may be in flight at a time so that protocol handling doesn't stall the bus.

This is uncommon among AXI4 implementations and almost unheard of in the example AXI-lite implementations I have examined.

Most AXI4 implementations will process a single burst transaction packet at a time and require some overhead to make this happen. Xilinx's AXI-lite implementations, both interconnect and slave implementations, only handle one request at a time. Other buses, such as Wishbone Classic, AHB, or APB, will only ever process one transaction word at a time.

If you are coming from AXI4, AXI-lite, or any one of these other bus implementations to the AXI4 or even AXI-lite components supported here, then you should expect to see a throughput increase by using one (or more) of the cores listed here--given of course that you have a bus master capable of issuing multiple requests at a time.

This performance improvement may be as significant as a 16x speedup when toggling an I/O, a 4x speedup when comparing this slave against Xilinx's block RAM memory controller (when processing single beat transactions), or as insignificant as 2% improvement from using the AXI4 MM to Slave converters (according to Xilinx's data sheets---I haven't yet run the test myself). This increased performance extends to the crossbar implementations contained within this repository as well, and so you may notice the improvement only increases when using these crossbars.

A Pipelined Wishbone B4 to AXI4 bridge

Built out of necessity, this repository was originally built around a Wishbone (WB) to AXI4 bridge, which is designed to provide a conversion from a (simpler) pipelined wishbone bus to an AXI4 bus for the purposes of driving memory transactions through Xilinx's SDRAM controllers. The WB->AXI bridge is designed to connect a wishbone bus to an AXI bus which may be wider--such as from a 32-bit WB bus to a 128-bit AXI bus. Hence, if the Memory Interface Generator DDR3 controller is running at a 4:1 clock rate, memory clocks to AXI system clocks, then this bus translator should be able to accomplish one transaction per clock at a sustained (pipelined) rate (neglecting any stalls due to refresh cycles).

Since the initial build of the core, I've added the WB to AXI lite bridge. This is also a pipelined bridge, and like the original one it has also been formally verified.

AXI to Wishbone conversion

While not the original purpose of the project, it now has both AXI-lite to WB and AXI to WB bridges. Each of these bridges comes in two parts, a read and write half. These halves can be used either independently, generating separate inputs to a WB crossbar, or combined through a WB arbiter.

The AXI-lite to WB bridge has been both formally verified and FPGA proven. This includes both the write half as well as the read half. Given the reluctance of the major vendors to support high speed AXI-lite interfaces, you aren't likely to find this kind of performance elsewhere.

The AXI to WB bridge write and read components have only been formally verified through about a dozen steps or so. This proof is deep enough to verify most of the bus interactions, but not nearly deep enough to verify any issues associated with internal FIFO overflows.

Wishbone pipeline to WB Classic

There's also a Wishbone (pipelined, master) to Wishbone (classic, slave) bridge, as well as the reverse Wishbone (classic, master) to Wishbone (pipelined, slave) bridge. Both of these have passed their formal tests. They are accompanied by a set of formal properties for Wishbone classic, both for slaves as well as masters.

AXI3 bridging

I'm now in the process of adding AXI3 bridges to this repository. These will be necessary for working with the Zynq chips, and others, that are still using AXI3. While the work is ongoing, I do have an AXI3 to AXI4 bridge available that's undergoing testing. The bridge supports two algorithms for W* reordering, and should be suitable for most applications.

Formal Verification

Currently, the project contains formal specifications for Avalon, Wishbone (classic), Wishbone (pipelined), APB, and AXI-lite buses. There's also a (partial) formal property specification for an AXI (full) bus, but the one in the master branch is incomplete. The complete set of AXI properties are maintained elsewhere. These properties, and the cores they've been used to verify, have all been tested and verified using SymbiYosys.

Xilinx Cores

The formal properties were first tested on a pair of Xilinx AXI demonstration cores. These cores failed formal verification. You can read about them on my blog, at zipcpu.com, here for AXI-lite and here for AXI. You can find the Xilinx cores referenced in those articles here and here for reference, for those who wish to repeat or examine my proofs.

Firewalls

A firewall is a guarantor: given an interface, of which only one side is trusted, the firewall guarantees the other side can trust the interface. More than that, a firewall can be used to trigger an in-circuit logic analyzer: if ever the interface rules are violated, the firewall will set an ouput fault indicator, which can then be used to trigger the logic analyzer. On top of that, the firewalls below are also built with an optional reset, allowing the design to safely return to functionality after triggering. In many cases, this requires resetting the downstream (untrusted) component.

  • AXILSAFETY is a bus fault isolator AXI-lite translator, sometimes called a firewall, designed to support a connection to a trusted AXI-lite master, and an untrusted AXI-lite slave. Should the slave attempt to return an illegal response, or perhaps a response beyond the user parameterized timeouts, then the untrusted slave will be "disconnected" from the bus, and a bus error will be returned for both the errant transaction and any following.

    AXILSAFETY also has a mode where, once a fault has been detected, the slave is reset and then allowed to return to the bus infrastructure again until its next fault.

    This core has been formally verified.

  • AXISAFETY is a bus fault isolator/firewall very similar to the AXILSAFETY bus fault isolator above with many of the same options. The difference is that the AXISAFETY core works with the full AXI4 specification, whereas the AXILSAFETY core works only with AXI4-lite.

    As with the AXILSAFETY example, the AXISAFETY firewall also has a mode where, once a fault has been detected, the slave is reset and allowed to return to the bus infrastructure until its next fault. Unliike the AXILSAFETY example, this one will only ever process a single AXI4 burst at a time.

    This core has been formally verified.

  • AXISSAFETY is a firewall for the AXI stream protocol. It guarantees the stream protocol, and optionally that the incoming stream will never be stalled for too long a period or that all packets downstream have the same length.

    This core has been formally verified.

  • WBSAFETY is a bus fault isolator/firewall, very similar to the AXILSAFETY firewall above, only for the Wishbone bus. Unlike many vendor firewall implementations, this one is able to reset the downstream core following any error without impacting it's ability to respond to the bus in a protocol compliant fashion.

    This core has been formally verified.

Cross-bars and AXI demonstrators

This repository has since become a repository for all kinds of bus-based odds and ends in addition to the bus translators mentioned above. Some of these odds and ends include crossbar switches and AXI demonstrator cores. As mentioned above, these cores are unique in their 100% throughput capabilities.

  • WBXBAR is a fully function N master to M slave Wishbone crossbar. Unlike my Unlike my earlier WB interconnects, this one guarantees that the ACK responses won't get crossed, and that misbehaving slave accesses will be timed out. The core also has options for checking for starvation (where a master's request is not granted in a particular period of time), double-buffering all outputs (i.e. with skid buffers, and forcing idle channel values to zero in order to reduce power.

    This core has been formally verified and used in several designs.

  • AXILXBAR is a fully functional, formally verified, N master to M slave AXI-lite crossbar interconnect. As such, it permits min(N,M) active channel connections between masters and slaves all at once. This core also has options for low power, whereby unused outputs are forced to zero, and lingering. Since the AXI protocol doesn't specify exactly when to close a channel, there's an OPT_LINGER allowing you to specify how many cycles the channel should be idle for in order for the channel to be closed. If the channel is not closed, a clock can be spared when reusing it. Otherwise, two clocks will be required to access a given channel.

    This core has been formally verified.

    While I haven't tested Xilinx's interconnect to know, if the quality of their demonstration AXI-lite slave core is any indication, then this cross-bar should easily outperform anything they have. The key unusual feature? The ability to maintain one transaction per clock over an extended period of time across any channel pair. (Their crossbar artificially limits AXI-lite interfaces to one transaction at a time.)

  • AXIL2AXIS converts from AXI-lite to AXI stream and back again. It's primary purpose is for testing AXI stream components at low speed, to make certain that they work before increasing the speed of the stream to the system clock rate. As such, writes to the core will generate writes to the AXI stream on the master side, and reads from the core will accept AXI stream reads on the slave side.

    While this isn't really intended to be a high performance core, it can still handle 100% throughput like most of my IP here. Therefore, anything less than 100% throughput through this core will be a test of and reflection of how the rest of your system works.

    This core has been formally verified.

  • AXIEMPTY is a cross bar helper. It's the simplest, most basic slave I could come up with that obeyed all the rules of AXI while returning a bus error for every request. It's designed to be used by the interconnect generator for those cases where there are no slaves on a given AXI bus.

    This core has been formally verified.

  • AXILEMPTY is a cross bar helper along the same lines as the AXIEMPTY core above. It has an nearly identical purpose, save only that AXILEMPTY is built to be the empty slave on an AXI-lite bus, not an AXI one.

    This core has been formally verified.

  • AXILSINGLE is designed to be a companion to AutoFPGA's AXI-lite support. It's purpose is to simplify connectivity logic when supporting multiple AXI-lite registers. This core takes a generic AXI-lite interface, and simplifies the interface so that multiple single-register cores can be connected to it at no loss in throughput. The single-register cores can either be full AXI-lite cores in their own respect, subject to simplification rules (listed within), or even further simplified from that. They must never stall the bus, and must always return responses within one clock cycle. The AXILSINGLE handles all backpressure issues. If done right, the backpressure logic from any downstream slave core will be removed by the synthesis tool, allowing all backpressure logic to be condensed into a few shared wires.

    This core has been formally verified.

  • AXILDOUBLE is the second AXI-lite companion to AutoFPGA's AXI-lite support. It's purpose is to simplify connectivity logic when supporting multiple AXI-lite slaves while imposing no throughput penalty. This core takes a generic AXI-lite interface, and simplifies the interface so that multiple peripherals can be connected to it. These peripheral cores can either be full AXI-lite cores in their own respect, subject to simplification rules discussed within, or even simplified from that. They must never stall the bus, and must always return responses within one clock cycle. The AXILDOUBLE core handles all backpressure issues, address selection, and invalid address returns.

    This core has been formally verified.

  • AXIXBAR is a fun project to develop a full NxM configurable crossbar using the full AXI protocol.

    Unique to this (full) AXI crossbar is the ability to have multiple ongoing transactions on each of the master-to-slave channels. Were Xilinx's crossbar to do this, it would've broken their demonstration AXI-full slave core.

    This core has been formally verified and used in several designs.

  • DEMOAXI is a demonstration AXI-lite slave core with more power and capability than Xilinx's demonstration AXI-lite slave core. Particular differences include 1) this one passes a formal verification check (Xilinx's core has bugs), and 2) this one can handle a maximum throughput of one transaction per clock. (Theirs did at best one transaction every other clock period.) You can read more about this demonstration AXI-lite slave core on ZipCPU.com in this article.

    This core has been formally verified.

  • EASYAXIL is a second demonstration AXI-lite slave core, only this time re-engineered to look and feel simpler than the DEMOAXI core above. It's also designed to use internal registers, vice a memory, so that it can be more easily extended. The core can either use skidbuffers, in which case its performance matches the DEMOAXI core above, or not, in which case it has only half the throughput. The real key difference is that the skid buffers have been separated into an external module.

    This core has been formally verified. While not used in any designs per se it has formed the basis for many successful AXI-lite designs.

  • AXILGPIO is a basic GPIO controller derived from the EASYAXIL design above.

    This core has been formally verified.

  • DEMOFULL is a fully capable AXI4 demonstration slave core rather than just the AXI-lite protocol. Well, okay, it doesn't do anything with the PROT, QOS, CACHE, and LOCK flags, so perhaps it isn't truly the full AXI protocol. Still, it's sufficient for most needs.

    Unlike Xilinx's demonstration AXI4 slave core, this one can handle 100% loading on both read and write channels simultaneously. That is, it can handle one read and one write beat per channel per clock with no stalls between bursts if the environment will allow it.

    This core has been formally verified and used in several designs.

  • AXI2AXILITE converts incoming AXI4 (full) requests for an AXI-lite slave. This conversion is fully pipelined, and capable of sending back to back AXI-lite requests on both channels.

    This core has been formally verified and used in several designs.

  • AXIS2MM converts an incoming stream signal into outgoinng AXI (full) requests. Supports bursting and aborted transactions. Also supports writes to a constant address, and continuous writes to concurrent addresses. This core depends upon all stream addresses being aligned.

    This core has been formally verified and checked in simulation.

  • AXIMM2S reads from a given address, and writes it to a FIFO buffer and then to an eventual AXI stream. Read requests are not issued unless room already exists in the FIFO, yet for a sufficiently fast stream the read requests may maintain 100% bus utilization--but only if the rest of the bus does as well. Supports continuous, fixed address or incrementing, and aborted transactions.

    Both this core and the one above it depend upon all stream words being aligned to the stream.

    This core has been both formally verified and checked in simulation.

  • AXIDMA is a hardware assisted memory copy. Given a source address, read address, and length, this core reads from the source address into a FIFO, and then writes the data from the FIFO to memory. As an optimization, memory address requests are not made unless the core is able to transfer at a 100% throughput rate.

    This core has been formally verified and used in several designs.

  • AXISGDMA is a brand new scatter-gather/vector-io based DMA controller. Give it a pointer to a table of DMA descriptors, and it will issue commands to the DMA until the table is complete.

    Both the internal FSM and the table reader have been separately verified. The AXISGDMA has not yet been verified.

  • AXIVCAMERA is a AXI-based frame-buffer writer. Given an AXI-stream video source, a frame start address, the number of lines in the image and the number of bytes per line, this core will copy one (or more) frames of video to memory.

    This core has been formally verified, and used successfully in a simulation based demonstration.

  • AXIVDISPLAY is a AXI-based frame-buffer source. Given a frame start address in memory, the number of lines in an image and the number of bytes per line, this core will perpetually read a video image from memory and produce it on an outgoing stream interface.

    This particular version can only handle bus aligned transfers.

    This core has been formally verified.

    You can find a demonstration of this core being used in my VGA simulator--supporting both VGA and HDMI outputs.

  • AXISINGLE is a (to be written) bus simplifier core along the lines of the AXILSINGLE, AXILDOUBLE and AXIDOUBLE cores, in that it can handle all of the bus logic for multiple AXI slaves while simplifying the bus interactions for each but at no throughput penalty. Once built, this will also be an AutoFPGA companion core. Slave's of type "SINGLE" (one register, one clock to generate a response) can be ganged together using it. This core will then essentially turn an AXI core into an AXI-lite core, with the same interface as AXILSINGLE above. When implemented, it will look very similar to the AXIDOUBLE core mentioned below.

  • AXIDOUBLE is the second AXI4 (full) companion to AutoFPGA's AXI4 (full) support. It's purpose is to simplify connectivity logic when supporting multiple AXI4 (full) slaves. This core takes a generic AXI4 (full) interface, and simplifies the interface so that peripherals can be connected to it with a minimal amount of logic. These peripherals cores can either be full AXI4 (full) cores in their own respect, subject to simplification rules discussed within, simplified AXI-lite slave as one might use with AXILDOUBLE, or even simpler than that. Key to this simplification is the assumption that the simplified slaves must never stall the bus, and that they must always return responses within one clock cycle. The AXIDOUBLE core handles all backpressure issues, ID logic, burst logic, address selection, invalid address return and exclusive access logic.

    This core has been formally verified.

  • WBXCLK can be used to cross clock domains on a pipelined Wishbone bus. It's conceptually an asynchronous request FIFO coupled with an asynchronous acknowledgment FIFO to cross clock domains. A counter in the original clock domain guarantees that the number of outstanding transactions remains smaller than the FIFO size. The design is complicated by the masters ability to arbitrarily lower CYC at any time mid-cycle and reliably be able to cancel any outgoing transactions in the downstream channel direction.

    This core has been formally verified.

  • APBXCLK can be used to cross clock domains on an APB bus. Unlike other solutions in this repository, this implementation is not pipelined--simply because the APB bus specification will not let it be so.

    This core has been formally verified.

  • AXIVFIFO implements a virtual FIFO. A virtual FIFO is basically a memory backed FIFO. Hence, after data gets written to this core it is then burst across an AXI bus to the whatever memory device is connected to the bus. This allows you to build FIFOs of arbitrarily large length for ... whatever task.

    This core has been formally verified.

  • AXIXCLK can be used to cross clock domains in an AXI context. As implemented, it is little more than a set of asynchronous FIFOs applied to each of the AXI channels. The asynchronous FIFOs have been formally verified,

  • AXIPERF is an AXI4 performance measurement peripheral. It has an AXI4 monitor interface, for use with monitoring an AXI4 (full) bus. A second AXI4-lite interface allows you to start, stop, or clear the data collection, as well as the ability to read the results back out. This core has been used to successfully measure bus latency and throughput, as well as to gain other valuable insights from any monitored AXI4 interface.

    This core has been demonstrated in simulation. The AXI-lite interface has been formally verified.

AXI Stream

  • AXISBROADCAST is a quick AXI stream processing engine that takes a single AXI-stream source, and "broadcasts" it to multiple downstream AXI-stream sinks.

    This core has been formally verified.

  • AXISPACKER packs AXI stream beats by removing bytes where TKEEP is zero.

    This core has been formally verified.

  • AXISRANDOM is a quick AXI stream source generating random numbers via a linear feedback shift register.

    This core has been formally verified.

  • AXISSWITCH is a quick switch for AXI streams. Given N stream inputs, select from among them to produce a stream output. Guarantees that the switch takes place at packet boundaries. Provides an AXI-lite interface for controlling which AXI stream gets forwarded downstream.

    This core has been formally verified.

APB

There are now two APB cores in this repository:

  • APBSLAVE is a demonstration APB slave.

    This core has been formally verified.

  • AXIL2APB -- a high throughput AXI-lite to APB bridge. Unlike other bridges, this one bridges to a single APB slave only. It can also maintain PSEL high across multiple bursts, achieving a maximum throughput rate of 50%.

    This core has been formally verified.

Frequently Asked Questions and Common Issues

  • default_nettype none

    It is my practice to set all of my design modules to default_nettype none. This tells the synthesis tool to generate an error any time I reference a signal which hasn't yet been defined. The default value, default_nettype wire, instructs the synthesis tool to instead generate a value, which will be a single bit of type wire, any time it sees an undefind value. The default also creates an opportunity for a misspelling to quickly turn into a design bug in many, many ways.

    The annoying part of default_nettype none is that all inputs must be declared as wires. input signal_name; is not good enough, it must be input wire signal_name;. I find this to be a small nuisance to pay for the tremendous benefit default_nettype none offers.

    Where this becomes a problem is when interfacing with other tools or other IP. Vivado HLS is known for producing logic which is not compatible with default_nettype none. I know of at least one ASIC foundary which produces simulation models for its components that are not default_nettype none safe. It's a common problem.

    One solution to this problem is to remove the default_nettype none line. This defeats the whole purpose of using the flag. Another solution is to place default_nettype wire at the bottom of the file at issue. For some tools (Yosys), this will also defeat the benefits of default_nettype none.

    A better solution is to fix the offending logic.

    An easier solution is to adjust the synthesis file order. Because Verilog directives are processed as though all of the files were concatenated together, a change of file order can often fix this issue.

Licensing

This repository is licensed under the Apache 2 license.

Thanks

I'd like to thank @wallento for his initial work on a Wishbone to AXI converter, and his encouragement to improve upon it. While this isn't a fork of his work, the initial pipelined wishbone to AXI bridge which formed the core seed for this project took its initial motivation from his work.

Many of the rest of these projects have been motivated by the desire to learn and develop my formal verification skills. For that, I would thank the staff of Symbiotic EDA for their tools and their encouragement.

wb2axip's People

Contributors

bogdanvuk avatar foobar2016 avatar zipcpu avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

wb2axip's Issues

Several files use the $clog2 function, which is not supported by Xilinx synthesis (at least 2016.4)

The following is a list when the $clog2 function is used:

bench/formal/faxis_master.v: ? 1 : $clog2(F_MAX_STALL+2);
bench/formal/faxis_slave.v: ? 1 : $clog2(F_MAX_STALL+2);
bench/formal/fwbc_slave.v: localparam DLYBITS= $clog2(F_MAX_DELAY+1);
bench/formal/axi_addr_miter.v: localparam DSZ = $clog2(DW)-3;
bench/formal/fwbc_master.v: localparam DLYBITS= $clog2(F_MAX_DELAY+1);
bench/formal/xlnxstream_2018_3.v: localparam F_LGDEPTH = $clog2(NUMBER_OF_OUTPUT_WORDS+1)+2;
rtl/axilwr2wbsp.v: localparam AXI_LSBS = $clog2(C_AXI_DATA_WIDTH)-3;
rtl/axilxbar.v: localparam LGLINGER = (OPT_LINGER>1) ? $clog2(OPT_LINGER+1) : 1;
rtl/axilxbar.v: localparam LGNM = (NM>1) ? $clog2(NM) : 1;
rtl/axilxbar.v: localparam LGNS = (NS>1) ? $clog2(NS+1) : 1;
rtl/axilxbar.v: // is $clog2(NS+1) rather than $clog2(NS). The extra bits
rtl/axilxbar.v: // reg [((NS>1)?$clog2(NS)-1:0):0] windex;
rtl/axilite2axi.v: assign M_AXI_AWSIZE = $clog2(C_AXI_DATA_WIDTH)-3;
rtl/axilite2axi.v: assign M_AXI_ARSIZE = $clog2(C_AXI_ADDR_WIDTH)-3;
rtl/axi_addr.v: localparam DSZ = $clog2(DW)-3;
rtl/axilrd2wbsp.v: localparam AXI_LSBS = $clog2(C_AXI_DATA_WIDTH)-3;
rtl/axi2axilite.v: localparam LSB = $clog2(C_AXI_DATA_WIDTH)-3;
rtl/axisafety.v: localparam LGTIMEOUT = $clog2(OPT_TIMEOUT+1);
rtl/axisafety.v: localparam LSB = $clog2(DW)-3;
rtl/wbm2axisp.v: localparam LG_AXI_DW = $clog2(C_AXI_DATA_WIDTH);
rtl/wbm2axisp.v: localparam LG_WB_DW = $clog2(DW);
rtl/wbm2axisp.v: localparam DWSIZE = $clog2(DW)-3;
rtl/wbm2axisp.v: // wire [(C_AXI_DATA_WIDTH>DW ? $clog2(C_AXI_DATA_WIDTH/DW):0)+$clog2(DW)-4:0] axi_lsbs;
rtl/wbm2axisp.v: wire [$clog2(DW)-4:0] axi_lsbs;
rtl/wbm2axisp.v: // wire [$clog2(DW)-4:0] axi_lsbs;
rtl/wbm2axisp.v: assume(f_const_addr[$clog2(DW)-4:0] == 0);
rtl/axixbar.v: localparam LGLINGER = (OPT_LINGER>1) ? $clog2(OPT_LINGER+1) : 1;
rtl/axixbar.v: localparam LGNM = (NM>1) ? $clog2(NM) : 1;
rtl/axixbar.v: localparam LGNS = (NS>1) ? $clog2(NS+1) : 1;
rtl/axixbar.v: // reg [((NM>1)?($clog2(NM)-1):0):0] rindex;
rtl/wbxbar.v: localparam TIMEOUT_WIDTH = $clog2(OPT_TIMEOUT);
rtl/wbxbar.v: localparam LGNM = (NM>1) ? $clog2(NM) : 1;
rtl/wbxbar.v: localparam LGNS = $clog2(NS+1);
rtl/demofull.v: localparam LSB = $clog2(C_S_AXI_DATA_WIDTH)-3;

However, this is not support by Xilinx Vivado Synthesis 2016.4 (I have not tried other versions as I am locked to 2016.4)

Recommend doing something like this to address:

https://stackoverflow.com/questions/5269634/address-width-from-ram-depth

`default_nettype none breaks vivado global synthesis

I've noticed some modules lead with

`default_nettype none

and at least one ends with

`ifndef	YOSYS
`default_nettype wire
`endif

It seems that without setting the type back to wire one will get very cryptic errors in vivado designs attempting global synthesis. For instance:

[Synth 8-6735] net type must be explicitly specified for 'ap_ready' when default_nettype is none
[Synth 8-1852] concurrent assignment to a non-net ap_ready is not permitted

directed towards sources of submodules of Vitis HLS gnerated blocks.

I've found this in both axis2mm.v and skidbuffer.v

High throughput AXI full master.

Not really an issue, just wondering if you already working/planning to make one and formally verify it so I won't duplicate the work.
Looking for high throughput AXI master with simple user interface similar to used in demofull.v
Thanks!

demofull incorrect read address generation in some scenarios.

The read address generation incorrectly depends on the present instead of latched values of ARBURST and ARLEN if the present value of either is non-zero. I think it's a typo in the ternary operator conditions where get_next_rd_addr is instantiated.

axi_addr #(.AW(AW), .DW(DW))
get_next_rd_addr((S_AXI_ARREADY ? S_AXI_ARADDR : raddr),
(S_AXI_ARREADY ? S_AXI_ARSIZE : rsize),
(S_AXI_ARBURST ? S_AXI_ARBURST: rburst), <- Typo here?
(S_AXI_ARLEN ? S_AXI_ARLEN : rlen), <= and here?
next_rd_addr);

For i_size and i_last_addr, this decides whether to use the current or latched version based on S_AXI_ARREADY, which makes sense. But for i_burst and i_len it decides current or latched based on the current value on the bus, which is incorrect. It means we are looking (and caring about) the values of the AR* signals when ARVALID && ARREADY is not true, this violating one of the fundamental rules of AXI.

As currently coded, if I request a 12-byte, INCR burst, and then reset all of the AR* data lines to X as soon as the transaction is accepted, then instead of an incrementing burst, I get the address (o_raddr) incrementing once, but all subsequent reads in the burst just re-use the same address. See simulation trace below.

Capture

Kicking off a transfer with AXIS2MM

Hi Dan, Managed to get the core implemented without too much trouble and have (I think) a rudimentary python driver (gist here) for in with PYNQ (interestingly the core shows up as a PYNQ Heirarchy around a DefaultIP, I suspect because of the way vivado wraps RTL in block designs).

The short of this is "How does one move the core from "idle" to "busy"?

From the ILA I see that data is passing through the core (WDATA is toggling) and after writing an address with my driver it is read back as I'd expect and I see AWADDR outputting the value I set so I don't seem to have an endian issue (0x500000000, the base address of some MIG DDR4 I'm using).

After writing length I can read that back and what I set it to impacts AWLEN but no writes have been issued. the command register always seems to be reading 0x90000, which I infer is telling me the FIFO is 512 long (as I set in vivado).

AWLEN started out at 255 (and stayed there for any large transactions), which as I understand it, is not a legal value for a burst with 256b TDATA (anything above 128 would cross a 4k boundary). Even if it is formally allowed, I've repeatedly seen xilinx docs that indicate crossing that boundary is not a good idea, so I'll be keeping an eye on if the smartconnect or MiG chokes.

I've looked though the verilog to see how I should tell the core to start and short of a couple of bits you have labeled as "reserved" but in fact seem to be related to start and prestart I'm drawing a blank.

Apologies if these implementation details aren't familiar or are largely irrelevant. I figure more (clear) info is better than less.

Finally, quick note on how I'm planning to use this: I feed it a stream that asserts TLAST between every other and every 256th clock (not transaction). So the stream will have between 2 and 256 beats every 256 clocks (generally this will be steady state, i.e. the same 128 beats out of 256 possible will be there every time, over and over). The core does not accept back pressure (its TREADY input is tied high as its fed from and ADC). I'd configure axis2mm to sync on TLAST (a very nice bonus) and capture some multiple of 32 (bytes) * N (active beats i.e. 128) * M (the number of sets I want, ~0.5-4 GiB of data). I'd start the core and let it spew unmolested into the MIG (which does have enough bandwidth) with it finishing after the total number of bytes and hopefully not griping that it has seen M TLAST assertions along the way.

Regarding err_state in WB to AXI 4 Lite Bridge

Hi,
When I was running write-read-write transaction then for 3rd i.e. write transaction I am not getting output (means ack or err any one is not generated) . can you help me in that . I have attached the screenshot. please check and let me know.
If someone provides me specification it will be very helpful.
write-read-write
write-Read-write_upper_part

Enhacement: Sync only on TLAST option for axis2mm

In testing the axis2mm core I've discovered, yet again, your documentation is true to its word, which has interesting consequences for our application.

OPT_TLAST_SYNC will synchronize the write with any incoming
packets. Packets are assumed to be synchronized initially
after any reset, or on the TVALID following any TLAST

In our situation I have a HLS core that filters beats out of the inbound axis stream and feeds then to axis2mm for capture. That core cannot accept back pressure so I've simply broken the TREADY line between it and axis2mm, as the TLAST sync feature ensures all will work. It does, but not on the first capture or the first capture after an abort and clearing on an error. In those cases axis2mm apparently considers itself freshly reset and hence in sync.

Presently my workaround is to simply make a small throwaway if the core has not captured anything or after an abort/clear error, but it would be convenient from a software perspective to have an option to sync only on TLAST and presume unsynced otherwise.

`default_nettype none causes issues when integrating with Xilinx IP

My build process is scripted and I cannot modify the Xilinx IP that attempts to integrate with these components.

I therefore have temporarily removed the `default_nettype none deceleration from these files and synthesis is able to progress (Vivado 2016.4), but the issue also shows up with Vivado 2018.3

  • Brendon

cannot index into non-array

[Synth 8-1751] cannot index into non-array reorder_fifo_valid ["b:/SVN/cores/customers/abc/wb2axip-master/rtl/src/wbm2axisp.v":565]

reorder_count not defined

[Synth 8-1031] reorder_count is not declared ["b:/SVN/cores/customers/abc/wb2axip-master/rtl/src/wbm2axisp.v":541]

Arbitration Behaviour of axixbar

In axixbar.v it says

// Note that this arbiter only forwards AxID fields. It does not use
// them in arbitration. As a result, only one master may ever make
// requests of any given slave at a time. All responses from a slave
// will be returned to that known master. This is a known limitation in
// this implementation which will be fixed (in time) with funding and
// interest. Until that time, in order for a second master to access
// a given slave, the first master must receive all of its acknowledgments.

I wonder if there's a "protection mechanism" or not, e.g.

  1. when one AXI master is waiting for the read response(of its read request) the other AXI master's ARREADY and AWREADY signals are de-asserted.
  2. ARREADY/AWREADY are de-asserted unless ARVALID/AWVALID is asserted (otherwise two AXI masters can issue read requests and xbar will accept them together).

Or it's the AXI masters' responsibility to not issue requests at the same time?

Looking forward to your reply.

the patreon support

Hi sir๏ผŒ
I found in the github issues that getting a formal property file like faxi_valaddr.v requires becoming a patreon member of zipcpu.

Since I am not familiar with the specific functions of using patreon, I would like to ask, if I want to learn related file content, do I only need to become a patreon member of zipcpu. I did not use a Google account to apply for github, so I was little confused about the follow-up process.

File 'faxi_valaddr.v' is missing

I was running SymbiYosys over .sby scripts in the repo, and encountered this error:

$ sby -f wbm2axisp.sby
SBY 17:15:33 [wbm2axisp_cvr] Removing directory '/home/jiegec/wb2axip/bench/formal/wbm2axisp_cvr'.
SBY 17:15:33 [wbm2axisp_cvr] Copy '/home/jiegec/wb2axip/rtl/wbm2axisp.v' to '/home/jiegec/wb2axip/bench/formal/wbm2axisp_cvr/src/wbm2axisp.v'.
SBY 17:15:33 [wbm2axisp_cvr] Copy '/home/jiegec/wb2axip/rtl/skidbuffer.v' to '/home/jiegec/wb2axip/bench/formal/wbm2axisp_cvr/src/skidbuffer.v'.
SBY 17:15:33 [wbm2axisp_cvr] Copy '/home/jiegec/wb2axip/bench/formal/faxi_master.v' to '/home/jiegec/wb2axip/bench/formal/wbm2axisp_cvr/src/faxi_master.v'.
SBY 17:15:33 [wbm2axisp_cvr] Copy '/home/jiegec/wb2axip/bench/formal/faxi_addr.v' to '/home/jiegec/wb2axip/bench/formal/wbm2axisp_cvr/src/faxi_addr.v'.
SBY 17:15:33 [wbm2axisp_cvr] Copy '/home/jiegec/wb2axip/bench/formal/faxi_valaddr.v' to '/home/jiegec/wb2axip/bench/formal/wbm2axisp_cvr/src/faxi_valaddr.v'.
Traceback (most recent call last):
  File "/home/jiegec/prefix/SymbiYosys/bin/sby", line 469, in <module>
    task_retcode = run_task(task)
  File "/home/jiegec/prefix/SymbiYosys/bin/sby", line 442, in run_task
    task.run(setupmode)
  File "/home/jiegec/prefix/SymbiYosys/bin/../share/yosys/python3/sby_core.py", line 683, in run
    self.copy_src()
  File "/home/jiegec/prefix/SymbiYosys/bin/../share/yosys/python3/sby_core.py", line 343, in copy_src
    copyfile(srcfile, dstfile)
  File "/usr/lib/python3.9/shutil.py", line 264, in copyfile
    with open(src, 'rb') as fsrc, open(dst, 'wb') as fdst:
FileNotFoundError: [Errno 2] No such file or directory: 'faxi_valaddr.v'

I could not find the missing file anywhere.

Icarus-verilog elaboration failed in axixbar.v

iverilog reports:

$ iverilog -g2012 ...
../../../submodules/wb2axip/rtl/axixbar.v:736: error: m_awvalid[N] is not a valid l-value in Main1.axiXbar_2.ip.UNUSED_WSKID_BUFFERS[3].
../../../submodules/wb2axip/rtl/axixbar.v:352:      : m_awvalid[N] is declared here as wire.
../../../submodules/wb2axip/rtl/axixbar.v:745: error: write_qos_lockout[N] is not a valid l-value in Main1.axiXbar_2.ip.UNUSED_WSKID_BUFFERS[3].
../../../submodules/wb2axip/rtl/axixbar.v:450:      : write_qos_lockout[N] is declared here as wire.

Offending code: https://github.com/ZipCPU/wb2axip/blob/master/rtl/axixbar.v#L735-L736 and https://github.com/ZipCPU/wb2axip/blob/master/rtl/axixbar.v#L744-L745

wbxbar slave-side STB remains asserted beyond ACK for one clock cycle for single word transaction.

I'm debugging an issue where LiteDRAM's Wishbone slave port locks up when attached to wbxbar.
The waveform shows that for an individual transaction, wbxbar's STB signal remains asserted for one clock cycle after the slave's ACK got deasserted. The slave interprets this as a new phase in a block cycle. The next clock cycle wbxbar aborts the transaction (deasserting CYC and STB) causing the slave to hang.
In the waveform you see on the slave port:

  1. The clock cycle before the cursor, STB is asserted and STALL is asserted.
  2. On the cursor, STALL is deasserted, ACK and STB are asserted.
  3. the next clock cycle shows ACK deasserted but STB still asserted.

image

Here is a snippet from the WB B4 spec describing how STB remaining asserted beyond the ACK pulse initiates a 2nd phase.

image

Here is my instantiation of the wbxbar:

localparam AW=28; //Bus address width
localparam DW=32; //Bus data width
localparam NUM_XBAR_MASTERS = 5;
localparam NUM_XBAR_SLAVES = 8;

wbxbar #(
.NM(NUM_XBAR_MASTERS), .NS(NUM_XBAR_SLAVES),
.AW(AW), .DW(32),
.SLAVE_ADDR(XBAR_SLAVE_ADDRS),
.SLAVE_MASK(XBAR_SLAVE_ADDR_MASKS),
.LGMAXBURST(3),
.OPT_DBLBUFFER(1'b0),
.OPT_LOWPOWER(1'b0))
wb_xbar (...)

Missing LICENSE file

Hi, looking forward to trying some of your formal verification tests against my own work. From your README, looks like the license is Apache 2.0. However, no LICENSE file currently exists in your repo, and github doesn't detect the license of your work. Dont suppose... please could you consider adding a LICENSE file to your repo? github will then pick this up, and automatically show the license type on the right hand side of your github page. (e.g. https://github.com/apache/httpd, see screenshot:

Screen Shot 2022-05-12 at 6 26 18 AM

something went wrong (I guess : the version of tools)

Hi Sir
I've been using your faxi_master recently, , but since the relevant parameter setting in the example I'm using is MAXBURST ==0, so I use the demofull example instead for burst-related behavior understanding.
However, when I performed sby -f demofull.sby, there were some errors that I did not understand, as follows

demofull_prf] base: starting process "cd demofull_prf/src; yosys -ql ../model/design.log ../model/design.ys"
[demofull_prflp] base: starting process "cd demofull_prflp/src; yosys -ql ../model/design.log ../model/design.ys"
[demofull_prf8lp] base: ERROR: Assert `modules_.count(module->name) == 0' failed in kernel/rtlil.cc:690.
[demofull_prf8lp] base: finished (returncode=1)
[demofull_prf8lp] base: task failed. ERROR.
 [demofull_prf8lp] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
[demofull_prf8lp] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
[demofull_prf8lp] summary: engine_0 (smtbmc boolector) did not return a status
 [demofull_prf8lp] summary: engine_0 did not produce any traces
 [demofull_prf8lp] DONE (ERROR, rc=16)
[demofull_prflp] base: ERROR: Assert `modules_.count(module->name) == 0' failed in kernel/rtlil.cc:690.
[demofull_prflck] base: starting process "cd demofull_prflck/src; yosys -ql ../model/design.log ../model/design.ys"
[demofull_prflp] base: finished (returncode=1)
 [demofull_prflp] base: task failed. ERROR.
 [demofull_prflp] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
[demofull_prflp] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
[demofull_prflp] summary: engine_0 (smtbmc boolector) did not return a status
 [demofull_prflp] DONE (ERROR, rc=16)

This information may seem verbose, but I just want to express as much as possible the error that I don't understand.
I used sby -f command to process skidbuffer, demoaxi, wbm2axisp and other files without any error message. However, the same error occurs in axidma.sby, aximm2s.sby, demofull.sby.
I tried to solve the problem by changing the version of the software in the symbiyosys I was using, or by downloading the binary program directly, but all failed. I wonder if I made some mistakes in using the software that I overlooked

JiaYan

compilation error in axi2axilite.v

Compiled with QuestSim-64-10.6c

** Error: ../hdl_cores/wb2axip/rtl/axi2axilite.v(443): (vlog-2110) Illegal reference to net "wfifo_empty".

** Error: ../hdl_cores/wb2axip/rtl/axi2axilite.v(444): (vlog-2110) Illegal reference to net "wfifo_full".

** Error: ../hdl_cores/wb2axip/rtl/axi2axilite.v(445): (vlog-2110) Illegal reference to net "wfifo_count".

** Error: ../hdl_cores/wb2axip/rtl/axi2axilite.v(447): (vlog-2110) Illegal reference to net "read_from_wrfifo".

** Error: ../hdl_cores/wb2axip/rtl/axi2axilite.v(624): (vlog-2110) Illegal reference to net "rfifo_empty".

** Error: ../hdl_cores/wb2axip/rtl/axi2axilite.v(625): (vlog-2110) Illegal reference to net "rfifo_full".

** Error: ../hdl_cores/wb2axip/rtl/axi2axilite.v(626): (vlog-2110) Illegal reference to net "rfifo_count".

Vivado Block design, local param, and axixbar

In making progress with the axis2mm core I've run into a 100% duty cycle issue with both the xilinx SmartConnect and Interconnect cores, so while I'm waiting on forum posts re:that I thought I'd give your axixbar core a whirl and try building up my own. I think I'm running into something related to #18. I'm also seeing similar complaint regarding axivfifo. This is in Vivado 2021.1

axixbar:

 [IP_Flow 19-350] User Parameter 'SLAVE_ADDR (Slave Addr)': Missing default value
 [IP_Flow 19-350] User Parameter 'SLAVE_MASK (Slave Mask)': Missing default value
 [IP_Flow 19-350] HDL Parameter 'SLAVE_ADDR (Slave Addr)': Missing default value
 [IP_Flow 19-627] HDL Parameter 'SLAVE_ADDR (Slave Addr)': XPath expression failed: Undefined parameter "AW" used in expression "{"111",{(AW - 3){"0"}},"110",{(AW - 3){"0"}},"101",{(AW - 3){"0"}},"100",{(AW - 3){"0"}},"011",{(AW - 3){"0"}},"010",{(AW - 3){"0"}},"0001",{(AW - 4){"0"}},"0000",{(AW - 4){"0"}}}".
 [IP_Flow 19-350] HDL Parameter 'SLAVE_MASK (Slave Mask)': Missing default value
 [IP_Flow 19-627] HDL Parameter 'SLAVE_MASK (Slave Mask)': XPath expression failed: Unbalanced parentheses found in expression "((spirit:decode(id('MODELPARAM_VALUE.NS')) <= 1) ? "1111",{(AW - 4){"0"}}} : {{(spirit:decode(id('MODELPARAM_VALUE.NS')) - 2){"111",{(AW - 3){"0"}}}},{2{"1111",{(AW - 4){"0"}}}})".

I was able to work around these issues by hard coding what I thought would be correct for a 2 to 1 512b data, 39b addr xbar and place the block. However the result is a block that would be very tedious to use as the axi interfaces are not separated properly. Compare the block with the xilinx crossbar:
Screen Shot 2022-01-23 at 8 55 07 PM
Screen Shot 2022-01-23 at 9 30 48 PM

axi2axilite

Hi!

first and foremost, thank you for your wonderful work!

I am currently employing some of your designs in order to simulate Verilog code generated by Vivado HLS. For some C inputs, the HLS generates RTL that locks up the whole FPGA and I am trying to find out whether this is a case of me not having understood the HLS good enough (wrong settings for bus latency, etc.) or whether this is a bug in the generated AXI Master implementation.

My first setup worked without problems and the HLS IP produced valid results:

 .โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€. 
(  Verilator TB   )
 `โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€' 
         m         
         โ”‚         
      axilite      
         โ”‚         
         s         
         โ–ผ         
    โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”     
    โ”‚ HLS IP โ”‚     
    โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜     
         m         
         โ”‚         
        axi        
         โ”‚         
         s         
         โ–ผ         
 โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”  
 โ”‚ axi2axilite  โ”‚  
 โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜  
         m         
         โ”‚         
      axilite      
         โ”‚         
         s         
   โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”   
   โ”‚ demoaxi.v โ”‚   
   โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜   

The Verilator TB starts (and waits for) the HLS IP via axilite and the bundled AXI master ports of the HLS IP are connected to memory via axi. I increased the address width of demoaxi.v and axi2axilite.v to 32 and also increased the 64 memory units in demoaxi.v to 1MiB in order order to mimic a memory controller.

I then tried to introduce some latency between axi2axilite and demoaxi.v by way of a pipeline stage, because the system that the HLS IP works in employs an Xilinx AXI interconnect (with additional latency). Since I am trying to find out why the HLS IP locks up that system I have to mimic its latency. The pipeline stage is conceptually depicted below. (Note that the number of daisy-chained DFFs can be configured.)

                        โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”                         โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”                    
                     โ”Œsโ”€โ”‚ HLS IP  โ”‚โ”€m                   sโ”Œโ”€โ–ถโ”‚ pipeline stage โ”‚โ”€mโ”€โ”                
                     โ”‚  โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜ โ”‚                    โ”‚  โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜   โ”‚                
                     โ”‚              โ”‚                    โ”‚                       โ”‚                
                     โ”‚             axi                axilite                 axilite             
                 axilite            โ”‚                    โ”‚                       โ”‚                
                     โ”‚              โ”‚                    โ”‚                       โ”‚                
 .โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€.   โ”‚              โ”‚  โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”  โ”‚                       โ”‚   โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”
(  Verilator TB   )โ—€โ”€m              sโ”€โ–ถโ”‚ axi2axilite  โ”‚mโ”€โ”˜                       sโ”€โ”€โ–ถโ”‚ demoaxi.v โ”‚
 `โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€'                     โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜                              โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜
------------------------------------------------------------------------------------
                                                                               โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”
โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”                                                           โ”‚              โ”‚
โ”‚                  โ”‚                                                           โ”‚              โ”‚
โ”‚                  โ”‚                                                           โ”‚              โ”‚
โ”‚                  โ”‚                 โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”                  โ”‚              โ”‚
โ”‚                  โ”‚ โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ–ถโ”‚ clock         DataOutโ”‚โ”€โ”€โ”€โ”€โ”€โ”€AWADDRโ”€โ”€โ”€โ”€โ–ถ โ”‚              โ”‚
โ”‚                  โ”‚                 โ”‚                      โ”‚                  โ”‚              โ”‚
โ”‚                  โ”‚ โ”€โ”€โ”€โ”€AWADDRโ”€โ”€โ”€โ”€โ”€โ–ถโ”‚ DataIn               โ”‚                  โ”‚              โ”‚
โ”‚                  โ”‚                 โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜                  โ”‚              โ”‚
โ”‚                  โ”‚                                                           โ”‚    demoaxi.v โ”‚
โ”‚axi2axilite.v     โ”‚                                                           โ”‚              โ”‚
โ”‚                  โ”‚                        โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”                         โ”‚              โ”‚
โ”‚                  โ”‚                        โ”‚  ...   โ”‚                         โ”‚              โ”‚
โ”‚                  โ”‚                        โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜                         โ”‚              โ”‚
โ”‚                  โ”‚                                                           โ”‚              โ”‚
โ”‚                  โ”‚                                                           โ”‚              โ”‚
โ”‚                  โ”‚                                                           โ”‚              โ”‚
โ”‚                  โ”‚                 โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”                  โ”‚              โ”‚
โ”‚                  โ”‚ โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ–ถโ”‚ clock         DataOutโ”‚โ—€โ”€โ”€โ”€โ”€ARREADYโ”€โ”€โ”€โ”€โ”€ โ”‚              โ”‚
โ”‚                  โ”‚                 โ”‚                      โ”‚                  โ”‚              โ”‚
โ”‚                  โ”‚ โ—€โ”€โ”€ARREADYโ”€โ”€โ”€โ”€โ”€โ”€โ”‚ DataIn               โ”‚                  โ”‚              โ”‚
โ”‚                  โ”‚                 โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜                  โ”‚              โ”‚
โ”‚                  โ”‚                                                           โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜
โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜                                                                           

With the additional latency, the HLS IP locked itself up. As far as I can tell from the simulation, the axi2axilite block does not return a BVALID to the HLS IP. I tried to increase LGFIFO to 4, 5, 6, and 32 which all yield the same results (a dead-lock). The demoaxi.v seems to return the write ack back to the axi2axilite though.

Is this a known limitation of the axi2axilite block? If so, how can I contribute?

I have a working symbiyosys setup and a little experience with it. Would it help if I try to add my axilite pipeline stage to increase the latency of the instance faxil_master in the FORMAL section of axi2axilite.v?

Best regards,
Florian

axisafety.v in ZYNQ Ultrascale+ works for read operations, but not for write operations

Hello,
I've been using axisafety.v in a ZYNQ-7000 firmware design very successfully. It reliably detects a missing AXI slave during read and write operations. However, in ZYNQ Ultrascale+, the behavior is different. The missing AXI slave is detected only for read operations. The bus is still blocked solid for any write operation to the missing slave. I have updated the code to the latest version available in this repository, but still seeing the same behavior.
Would it be possible to fix that?
thanks.

axisafety module fails tests with ZYNQ + AXI BRAM controller

Hello,
first of all, this is a very useful collection of utilities, thanks a lot for making them available.
My issue:
I'm trying to use axisafety module to prevent AXI bus lockups. As a first step, I tried testing it with a known-good module, which is Xilinx standard AXI BRAM controller. Steps are below:

  1. Had to convert all localparams into params in axisafety.v source, otherwise Vivado schematic editor does not recognize the module as valid for inclusion into schematics. (Using Vivado 2020.1)
  2. Connected AXI BRAM controller with BRAM attached directly to ZYNQ AXI interconnect, verified that it works by writing and reading from Linux console using devmem utility. Writing a number into address 0x50000000 and then reading it back returns the number that was written. (0x50000000 is BRAM base address)
  3. Attached axisafety module between AXI interconnect and AXI BRAM controller. See attached pictures for details. BRAM depth is 8KB.
  4. When trying to write/read the BRAM using devmem utility, both read and write operations are successful, but the value read back is always 0. It does not depend on what was previously written into BRAM.

Could you let me know if axisafety was attached and configured correctly? If not, what must be changed?

thanks.
Alex Madorsky
University of Florida/Physics.

image
image
image

Possible enhancement: add AWCACHE parameter to axis2mm

In exploring design options for our larger system I've discovered that xilinx's documentation for their AXI data width converter will only pack bursts when upsizing if AWCACHE[1] (I think) is set. Presently I've simply hardcoded b0011 to test (and I think I see how to add it to the verilog with a pull request. As my HDL is extremely limited I thought instead I'd call your attention to this as a potential enhancement that might help with downstream throughput.

illegal localparam in list of parameters

Hi,

It is illegal to use localparam in the parameter list.
For NC, it will report an error:
file: axixbar.v
localparam IW = C_AXI_ID_WIDTH,
|
ncvlog: *E,LOCALP (axixbar.v,103|11): illegal localparam in list of parameters [12.2(IEEE-2001)].
localparam AW = C_AXI_ADDR_WIDTH,
|
ncvlog: *E,LOCALP (axixbar.v,104|11): illegal localparam in list of parameters [12.2(IEEE-2001)].
localparam DW = C_AXI_DATA_WIDTH,
|

For VCS,
the localparma will have some misbehave. (not changed w/ parameter assign)

xlnxdemo formal verification fails

When I run sby -f xlnxdemo.sby with the FOSS yosys version (just built the master branch at 19d6b8846f55b4c7be705619f753bec86deadac8)

I get this:

SBY 14:52:58 [xlnxdemo_cvr] Removing direcory 'xlnxdemo_cvr'.
SBY 14:52:58 [xlnxdemo_cvr] Copy 'faxil_slave.v' to 'xlnxdemo_cvr/src/faxil_slave.v'.
SBY 14:52:58 [xlnxdemo_cvr] Copy 'xlnxdemo.v' to 'xlnxdemo_cvr/src/xlnxdemo.v'.
SBY 14:52:58 [xlnxdemo_cvr] engine_0: smtbmc
SBY 14:52:58 [xlnxdemo_cvr] base: starting process "cd xlnxdemo_cvr/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 14:52:59 [xlnxdemo_cvr] base: finished (returncode=0)
SBY 14:52:59 [xlnxdemo_cvr] smt2: starting process "cd xlnxdemo_cvr/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 14:52:59 [xlnxdemo_cvr] smt2: finished (returncode=0)
SBY 14:52:59 [xlnxdemo_cvr] engine_0: starting process "cd xlnxdemo_cvr; yosys-smtbmc --presat --unroll -c --noprogress -t 60 --append 0 --dump-vcd engine_0/trace%.vcd --dump-vlogtb engine_0/trace%_tb.v --dump-smtc engine_0/trace%.smtc model/design_smt2.smt2"
SBY 14:52:59 [xlnxdemo_cvr] engine_0: ##   0:00:00  Solver: yices
SBY 14:52:59 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 0..
SBY 14:52:59 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 1..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Reached cover statement at xlnxdemo.v:798 in step 1.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace0.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace0_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace0.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 1..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Reached cover statement at xlnxdemo.v:788 in step 1.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace1.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace1_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace1.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 1..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 2..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Reached cover statement at xlnxdemo.v:1019 in step 2.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace2.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace2_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace2.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 2..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Reached cover statement at xlnxdemo.v:901 in step 2.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace3.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace3_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace3.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 2..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:00  Checking cover reachability in step 3..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at xlnxdemo.v:902 in step 3.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace4.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace4_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace4.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 3..
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at xlnxdemo.v:1020 in step 3.
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace5.vcd
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace5_tb.v
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace5.smtc
SBY 14:53:00 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 3..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 4..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at xlnxdemo.v:1021 in step 4.
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace6.vcd
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace6_tb.v
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace6.smtc
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 4..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at xlnxdemo.v:903 in step 4.
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace7.vcd
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace7_tb.v
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace7.smtc
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 4..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 5..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Reached cover statement at faxil_slave.v:704 in step 5.
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to VCD file: engine_0/trace8.vcd
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to Verilog testbench: engine_0/trace8_tb.v
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Writing trace to constraints file: engine_0/trace8.smtc
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:01  Checking cover reachability in step 5..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at xlnxdemo.v:904 in step 5.
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace9.vcd
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to Verilog testbench: engine_0/trace9_tb.v
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to constraints file: engine_0/trace9.smtc
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 5..
SBY 14:53:01 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at faxil_slave.v:697 in step 5.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace10.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to Verilog testbench: engine_0/trace10_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to constraints file: engine_0/trace10.smtc
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 5..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at xlnxdemo.v:1022 in step 5.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace11.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to Verilog testbench: engine_0/trace11_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to constraints file: engine_0/trace11.smtc
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 5..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 6..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at xlnxdemo.v:1023 in step 6.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace12.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to Verilog testbench: engine_0/trace12_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to constraints file: engine_0/trace12.smtc
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Checking cover reachability in step 6..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Reached cover statement at xlnxdemo.v:792 in step 6.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:02  Writing trace to VCD file: engine_0/trace13.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to Verilog testbench: engine_0/trace13_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to constraints file: engine_0/trace13.smtc
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 6..
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Reached cover statement at xlnxdemo.v:905 in step 6.
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to VCD file: engine_0/trace14.vcd
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to Verilog testbench: engine_0/trace14_tb.v
SBY 14:53:02 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to constraints file: engine_0/trace14.smtc
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 6..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 7..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Reached cover statement at xlnxdemo.v:906 in step 7.
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to VCD file: engine_0/trace15.vcd
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to Verilog testbench: engine_0/trace15_tb.v
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to constraints file: engine_0/trace15.smtc
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 7..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Reached cover statement at xlnxdemo.v:817 in step 7.
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to VCD file: engine_0/trace16.vcd
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to Verilog testbench: engine_0/trace16_tb.v
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to constraints file: engine_0/trace16.smtc
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Checking cover reachability in step 7..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Reached cover statement at xlnxdemo.v:810 in step 7.
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:03  Writing trace to VCD file: engine_0/trace17.vcd
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to Verilog testbench: engine_0/trace17_tb.v
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to constraints file: engine_0/trace17.smtc
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 7..
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Reached cover statement at xlnxdemo.v:1024 in step 7.
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to VCD file: engine_0/trace18.vcd
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to Verilog testbench: engine_0/trace18_tb.v
SBY 14:53:03 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to constraints file: engine_0/trace18.smtc
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 7..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 8..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Reached cover statement at xlnxdemo.v:1025 in step 8.
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to VCD file: engine_0/trace19.vcd
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to Verilog testbench: engine_0/trace19_tb.v
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to constraints file: engine_0/trace19.smtc
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 8..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Reached cover statement at xlnxdemo.v:907 in step 8.
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to VCD file: engine_0/trace20.vcd
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to Verilog testbench: engine_0/trace20_tb.v
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Writing trace to constraints file: engine_0/trace20.smtc
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:04  Checking cover reachability in step 8..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 9..
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:05  Reached cover statement at xlnxdemo.v:1026 in step 9.
SBY 14:53:04 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to VCD file: engine_0/trace21.vcd
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to Verilog testbench: engine_0/trace21_tb.v
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to constraints file: engine_0/trace21.smtc
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 9..
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Reached cover statement at xlnxdemo.v:908 in step 9.
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to VCD file: engine_0/trace22.vcd
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to Verilog testbench: engine_0/trace22_tb.v
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to constraints file: engine_0/trace22.smtc
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 9..
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 10..
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Reached cover statement at xlnxdemo.v:1027 in step 10.
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to VCD file: engine_0/trace23.vcd
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to Verilog testbench: engine_0/trace23_tb.v
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Writing trace to constraints file: engine_0/trace23.smtc
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:05  Checking cover reachability in step 10..
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Reached cover statement at xlnxdemo.v:909 in step 10.
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to VCD file: engine_0/trace24.vcd
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to Verilog testbench: engine_0/trace24_tb.v
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to constraints file: engine_0/trace24.smtc
SBY 14:53:05 [xlnxdemo_cvr] engine_0: ##   0:00:06  Checking cover reachability in step 10..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Checking cover reachability in step 11..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Reached cover statement at xlnxdemo.v:1028 in step 11.
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to VCD file: engine_0/trace25.vcd
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to Verilog testbench: engine_0/trace25_tb.v
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to constraints file: engine_0/trace25.smtc
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Checking cover reachability in step 11..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Reached cover statement at xlnxdemo.v:910 in step 11.
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to VCD file: engine_0/trace26.vcd
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to Verilog testbench: engine_0/trace26_tb.v
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Writing trace to constraints file: engine_0/trace26.smtc
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:06  Checking cover reachability in step 11..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:07  Checking cover reachability in step 12..
SBY 14:53:06 [xlnxdemo_cvr] engine_0: ##   0:00:07  Reached cover statement at xlnxdemo.v:911 in step 12.
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to VCD file: engine_0/trace27.vcd
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to Verilog testbench: engine_0/trace27_tb.v
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to constraints file: engine_0/trace27.smtc
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Checking cover reachability in step 12..
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Checking cover reachability in step 13..
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Reached cover statement at xlnxdemo.v:912 in step 13.
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to VCD file: engine_0/trace28.vcd
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to Verilog testbench: engine_0/trace28_tb.v
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Writing trace to constraints file: engine_0/trace28.smtc
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:07  Checking cover reachability in step 13..
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:08  Reached cover statement at xlnxdemo.v:1029 in step 13.
SBY 14:53:07 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to VCD file: engine_0/trace29.vcd
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to Verilog testbench: engine_0/trace29_tb.v
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to constraints file: engine_0/trace29.smtc
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Checking cover reachability in step 13..
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Checking cover reachability in step 14..
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Reached cover statement at xlnxdemo.v:1030 in step 14.
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to VCD file: engine_0/trace30.vcd
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to Verilog testbench: engine_0/trace30_tb.v
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to constraints file: engine_0/trace30.smtc
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Checking cover reachability in step 14..
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Reached cover statement at xlnxdemo.v:913 in step 14.
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:08  Writing trace to VCD file: engine_0/trace31.vcd
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to Verilog testbench: engine_0/trace31_tb.v
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to constraints file: engine_0/trace31.smtc
SBY 14:53:08 [xlnxdemo_cvr] engine_0: ##   0:00:09  Checking cover reachability in step 14..
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Checking cover reachability in step 15..
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Reached cover statement at xlnxdemo.v:1031 in step 15.
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to VCD file: engine_0/trace32.vcd
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to Verilog testbench: engine_0/trace32_tb.v
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Writing trace to constraints file: engine_0/trace32.smtc
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Checking cover reachability in step 15..
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:09  Checking cover reachability in step 16..
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:10  Reached cover statement at xlnxdemo.v:1032 in step 16.
SBY 14:53:09 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to VCD file: engine_0/trace33.vcd
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to Verilog testbench: engine_0/trace33_tb.v
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to constraints file: engine_0/trace33.smtc
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Checking cover reachability in step 16..
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Checking cover reachability in step 17..
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Reached cover statement at xlnxdemo.v:1033 in step 17.
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to VCD file: engine_0/trace34.vcd
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to Verilog testbench: engine_0/trace34_tb.v
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Writing trace to constraints file: engine_0/trace34.smtc
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:10  Checking cover reachability in step 17..
SBY 14:53:10 [xlnxdemo_cvr] engine_0: ##   0:00:11  Checking cover reachability in step 18..
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Reached cover statement at xlnxdemo.v:1034 in step 18.
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Writing trace to VCD file: engine_0/trace35.vcd
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Writing trace to Verilog testbench: engine_0/trace35_tb.v
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Writing trace to constraints file: engine_0/trace35.smtc
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Checking cover reachability in step 18..
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Checking cover reachability in step 19..
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:11  Reached cover statement at xlnxdemo.v:1035 in step 19.
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to VCD file: engine_0/trace36.vcd
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to Verilog testbench: engine_0/trace36_tb.v
SBY 14:53:11 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to constraints file: engine_0/trace36.smtc
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Checking cover reachability in step 19..
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Checking cover reachability in step 20..
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Reached cover statement at xlnxdemo.v:1036 in step 20.
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to VCD file: engine_0/trace37.vcd
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to Verilog testbench: engine_0/trace37_tb.v
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Writing trace to constraints file: engine_0/trace37.smtc
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:12  Checking cover reachability in step 20..
SBY 14:53:12 [xlnxdemo_cvr] engine_0: ##   0:00:13  Checking cover reachability in step 21..
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Reached cover statement at xlnxdemo.v:1037 in step 21.
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Writing trace to VCD file: engine_0/trace38.vcd
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Writing trace to Verilog testbench: engine_0/trace38_tb.v
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Writing trace to constraints file: engine_0/trace38.smtc
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Checking cover reachability in step 21..
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:13  Checking cover reachability in step 22..
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:14  Reached cover statement at xlnxdemo.v:1038 in step 22.
SBY 14:53:13 [xlnxdemo_cvr] engine_0: ##   0:00:14  Writing trace to VCD file: engine_0/trace39.vcd
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Writing trace to Verilog testbench: engine_0/trace39_tb.v
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Writing trace to constraints file: engine_0/trace39.smtc
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Checking cover reachability in step 22..
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Checking cover reachability in step 23..
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Reached cover statement at xlnxdemo.v:1039 in step 23.
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:14  Writing trace to VCD file: engine_0/trace40.vcd
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:15  Writing trace to Verilog testbench: engine_0/trace40_tb.v
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:15  Writing trace to constraints file: engine_0/trace40.smtc
SBY 14:53:14 [xlnxdemo_cvr] engine_0: ##   0:00:15  Checking cover reachability in step 23..
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:15  Checking cover reachability in step 24..
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:15  Reached cover statement at xlnxdemo.v:1040 in step 24.
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:15  Writing trace to VCD file: engine_0/trace41.vcd
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:15  Writing trace to Verilog testbench: engine_0/trace41_tb.v
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:16  Writing trace to constraints file: engine_0/trace41.smtc
SBY 14:53:15 [xlnxdemo_cvr] engine_0: ##   0:00:16  Checking cover reachability in step 24..
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Checking cover reachability in step 25..
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Reached cover statement at xlnxdemo.v:1041 in step 25.
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Writing trace to VCD file: engine_0/trace42.vcd
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Writing trace to Verilog testbench: engine_0/trace42_tb.v
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Writing trace to constraints file: engine_0/trace42.smtc
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:16  Checking cover reachability in step 25..
SBY 14:53:16 [xlnxdemo_cvr] engine_0: ##   0:00:17  Checking cover reachability in step 26..
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Reached cover statement at xlnxdemo.v:1042 in step 26.
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Writing trace to VCD file: engine_0/trace43.vcd
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Writing trace to Verilog testbench: engine_0/trace43_tb.v
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Writing trace to constraints file: engine_0/trace43.smtc
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Checking cover reachability in step 26..
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:17  Checking cover reachability in step 27..
SBY 14:53:17 [xlnxdemo_cvr] engine_0: ##   0:00:18  Checking cover reachability in step 28..
SBY 14:53:18 [xlnxdemo_cvr] engine_0: ##   0:00:18  Checking cover reachability in step 29..
SBY 14:53:18 [xlnxdemo_cvr] engine_0: ##   0:00:18  Checking cover reachability in step 30..
SBY 14:53:18 [xlnxdemo_cvr] engine_0: ##   0:00:18  Checking cover reachability in step 31..
SBY 14:53:18 [xlnxdemo_cvr] engine_0: ##   0:00:19  Checking cover reachability in step 32..
SBY 14:53:19 [xlnxdemo_cvr] engine_0: ##   0:00:19  Checking cover reachability in step 33..
SBY 14:53:19 [xlnxdemo_cvr] engine_0: ##   0:00:19  Checking cover reachability in step 34..
SBY 14:53:19 [xlnxdemo_cvr] engine_0: ##   0:00:20  Checking cover reachability in step 35..
SBY 14:53:20 [xlnxdemo_cvr] engine_0: ##   0:00:20  Checking cover reachability in step 36..
SBY 14:53:20 [xlnxdemo_cvr] engine_0: ##   0:00:20  Checking cover reachability in step 37..
SBY 14:53:20 [xlnxdemo_cvr] engine_0: ##   0:00:20  Checking cover reachability in step 38..
SBY 14:53:20 [xlnxdemo_cvr] engine_0: ##   0:00:21  Checking cover reachability in step 39..
SBY 14:53:21 [xlnxdemo_cvr] engine_0: ##   0:00:21  Checking cover reachability in step 40..
SBY 14:53:21 [xlnxdemo_cvr] engine_0: ##   0:00:21  Checking cover reachability in step 41..
SBY 14:53:21 [xlnxdemo_cvr] engine_0: ##   0:00:22  Checking cover reachability in step 42..
SBY 14:53:22 [xlnxdemo_cvr] engine_0: ##   0:00:22  Checking cover reachability in step 43..
SBY 14:53:22 [xlnxdemo_cvr] engine_0: ##   0:00:22  Checking cover reachability in step 44..
SBY 14:53:22 [xlnxdemo_cvr] engine_0: ##   0:00:22  Checking cover reachability in step 45..
SBY 14:53:23 [xlnxdemo_cvr] engine_0: ##   0:00:23  Checking cover reachability in step 46..
SBY 14:53:23 [xlnxdemo_cvr] engine_0: ##   0:00:23  Checking cover reachability in step 47..
SBY 14:53:23 [xlnxdemo_cvr] engine_0: ##   0:00:23  Checking cover reachability in step 48..
SBY 14:53:24 [xlnxdemo_cvr] engine_0: ##   0:00:24  Checking cover reachability in step 49..
SBY 14:53:24 [xlnxdemo_cvr] engine_0: ##   0:00:24  Checking cover reachability in step 50..
SBY 14:53:24 [xlnxdemo_cvr] engine_0: ##   0:00:24  Checking cover reachability in step 51..
SBY 14:53:25 [xlnxdemo_cvr] engine_0: ##   0:00:25  Checking cover reachability in step 52..
SBY 14:53:25 [xlnxdemo_cvr] engine_0: ##   0:00:25  Checking cover reachability in step 53..
SBY 14:53:25 [xlnxdemo_cvr] engine_0: ##   0:00:26  Checking cover reachability in step 54..
SBY 14:53:26 [xlnxdemo_cvr] engine_0: ##   0:00:26  Checking cover reachability in step 55..
SBY 14:53:26 [xlnxdemo_cvr] engine_0: ##   0:00:26  Checking cover reachability in step 56..
SBY 14:53:26 [xlnxdemo_cvr] engine_0: ##   0:00:27  Checking cover reachability in step 57..
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:27  Checking cover reachability in step 58..
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:27  Checking cover reachability in step 59..
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:28  Unreached cover statement at xlnxdemo.v:829.
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:28  Unreached cover statement at xlnxdemo.v:836.
SBY 14:53:27 [xlnxdemo_cvr] engine_0: ##   0:00:28  Status: FAILED (!)
SBY 14:53:27 [xlnxdemo_cvr] engine_0: finished (returncode=1)
SBY 14:53:27 [xlnxdemo_cvr] engine_0: Status returned by engine: FAIL
SBY 14:53:27 [xlnxdemo_cvr] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:29 (29)
SBY 14:53:27 [xlnxdemo_cvr] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:30 (30)
SBY 14:53:27 [xlnxdemo_cvr] summary: engine_0 (smtbmc) returned FAIL
SBY 14:53:27 [xlnxdemo_cvr] DONE (FAIL, rc=2)
SBY 14:53:27 [xlnxdemo_prf] Removing direcory 'xlnxdemo_prf'.
SBY 14:53:27 [xlnxdemo_prf] Copy 'faxil_slave.v' to 'xlnxdemo_prf/src/faxil_slave.v'.
SBY 14:53:27 [xlnxdemo_prf] Copy 'xlnxdemo.v' to 'xlnxdemo_prf/src/xlnxdemo.v'.
SBY 14:53:27 [xlnxdemo_prf] engine_0: smtbmc
SBY 14:53:27 [xlnxdemo_prf] base: starting process "cd xlnxdemo_prf/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 14:53:28 [xlnxdemo_prf] base: finished (returncode=0)
SBY 14:53:28 [xlnxdemo_prf] smt2: starting process "cd xlnxdemo_prf/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 14:53:29 [xlnxdemo_prf] smt2: finished (returncode=0)
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: starting process "cd xlnxdemo_prf; yosys-smtbmc --presat --unroll --noprogress -t 40 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: starting process "cd xlnxdemo_prf; yosys-smtbmc --presat --unroll -i --noprogress -t 40 --append 0 --dump-vcd engine_0/trace_induct.vcd --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2"
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Solver: yices
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Solver: yices
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 0..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 0..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 40..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 39..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 1..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 1..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 38..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 2..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 2..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 37..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 36..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 3..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 3..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 35..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 4..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 4..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 34..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 5..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 5..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 33..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 32..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assumptions in step 6..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Checking assertions in step 6..
SBY 14:53:29 [xlnxdemo_prf] engine_0.induction: ##   0:00:00  Trying induction in step 31..
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  BMC failed!
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Assert failed in xlnxdemo: xlnxdemo.v:774
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 14:53:29 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 14:53:30 [xlnxdemo_prf] engine_0.basecase: ##   0:00:00  Status: FAILED (!)
SBY 14:53:30 [xlnxdemo_prf] engine_0.basecase: finished (returncode=1)
SBY 14:53:30 [xlnxdemo_prf] engine_0: Status returned by engine for basecase: FAIL
SBY 14:53:30 [xlnxdemo_prf] engine_0.induction: terminating process
SBY 14:53:30 [xlnxdemo_prf] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:02 (2)
SBY 14:53:30 [xlnxdemo_prf] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:02 (2)
SBY 14:53:30 [xlnxdemo_prf] summary: engine_0 (smtbmc) returned FAIL for basecase
SBY 14:53:30 [xlnxdemo_prf] summary: counterexample trace: xlnxdemo_prf/engine_0/trace.vcd
SBY 14:53:30 [xlnxdemo_prf] DONE (FAIL, rc=2)

Unfortunately I'm too much of a beginner to figure out where the issues is. I can also provide the vcd files if you can't reproduce.

axi2axilite.v: M_AXI_BVALID does not propagate to S_AXI_BVALID

Performing a AXI4 to WB conversion using the recommended components (per the repo's README.md)

Issued a single write, which successfully propagated to the WB target. The axlite2wbsp component successfully generates the the assertion of M_AXI_BVALID, but I never see S_AXI_BVALID asserted.

Waveforms attached. Parameters set to default with the exception of LGFIFO = 1

axi2axilite_1
axi2axilite_2

fusesoc file based on CAPI 1 standard.

fusesoc has moved to the CAPI 2 standard for its core description files. The current core file wb2axip.core is CAPI 1 and will cause fusesoc to give an error to the end user. Recommend removing it to avoid confusion.

Future Improvement: individual fusesoc core files in the repo, if this is something you would like let me know and I'll get it done.

Question regarding AW / W channel dependencies

Note: This is not an issue, but merely a notice to Mr. ZipCPU. Since I am certain from reading his blog that he is a very busy man indeed, I thought this is the right place to put this.

I came here after reading the blog post "The hard part of building a bursting AXI Master," which was very helpful for me indeed, since I'm about to write an AXI DMA myself. (Once I have the time.)
Here the problem of generating a AW transaction was solved by the use of "phantom signals," or to put it in other words, 'doing the AW calculation for the next burst transfer in the three cycles at the beginning of the current burst transfer.'
However, by using Xilinx's core I came previously across the fact that W transactions may take place before the associated AW transaction and this is also explicitly stated in the AXI specification:

"This means, for example, that the write data can appear at an interface before the write address for the transaction.
This can occur if the write address channel contains more register stages than the write data channel. Similarly, the
write data might appear in the same cycle as the address."
(A3.3, AMBA AXI and ACE Protocol Specification)

That is, this problem may also be solved by simply delaying the AW transaction by the required amount of cycles, while issuing the W requests right away. (Xilinx's deprecated AXI Master Burst does this and issues the AW transaction 3 cycles later.)

I have observed in your design, that in burst transactions the AW transaction is always issued synchronously to the first associated W transaction. (Such as in Fig. 10 of aforementioned blog post.)
Is there any practical reason you obey to this additional rule?
In the past I've heard about IP cores that do not work properly because they aren't designed for this case. Maybe this is the reason?

axim2wbsp.v: has different data endianness for write and read channels

Hello,

There's a problem in AXI2Wishbone bridge. On a write channel the data on the write channel gets nibble-inverted, while on the read channel it's passed without modification.
After a bit of investigation I've found that this is most likely caused by different default generics:
aximwr2wbsp.v:

		parameter [0:0] OPT_SWAP_ENDIANNESS = 1'b1,

aximrd2wbsp.v:

		parameter [0:0] OPT_SWAP_ENDIANNESS = 1'b0,

I believe that's not really a user-preferred behavior.
Maybe the best option would be to add this generic to axim2wbsp.v and just pass it to instantiated modules?

AXIS2MM & WUSER bits/byte causes critical warning in Vivado

Hi Dan,
First a disclaimer this may well not be an issue with axis2mm.v and merely a cosmetic interplay with Vivado's IP Validation system. I'm trying to test the core in a design I'm presently having HLS issues with the same task. The inbound stream consists of TLAST, TDATA (256b), and no TUSER (TKEEP, and TSTRB are there but ripped out in implementation as I don't use them and HLS insists on placing them on blocks).

I've configured your core, whose output is routed to a SmartConnect with a null TUSER width but I see in the verilog that that still results in a single wire for TUSER in and out. This results in a critical warning in validation (which I'm attempting to ignore):
[xilinx.com:ip:smartconnect:1.0-1] capture_play_axi_smc_1: WUSER_WIDTH (1) of S00_AXI must be integer number of bits per byte of WDATA (256). And as I understand it that warning is based on the AXI4 standard.

I suspect this isn't strictly a bug, but given the effort you've put into these blocks (but have not tested this one in a design per your docs) I thought you might be interested.

I've got your core configured as below, I'll be interested to see how it holds up with a 512MHz clock and a 4GiB max transfer of a 256b stream.

		parameter	C_AXI_ADDR_WIDTH = 36,
		parameter	C_AXI_DATA_WIDTH = 256,
		parameter	C_AXI_ID_WIDTH = 1,
		parameter	C_AXIS_TUSER_WIDTH = 0,
		parameter [0:0]	OPT_TLAST_SYNC = 1,
		parameter [0:0]	OPT_TREADY_WHILE_IDLE = 1,
		parameter [7:0]	ABORT_KEY = 8'h26,
		parameter	LGFIFO = 9,
		parameter	LGLEN  = 32,
		parameter [C_AXI_ID_WIDTH-1:0]	AXI_ID = 0,
		parameter	[0:0]	OPT_LOWPOWER  = 1'b0,
		parameter	[0:0]	OPT_CLKGATE   = OPT_LOWPOWER

always block with constant assignment

Hi

Disclaimer: I'm rather VHDL... The last Verilog training is some years ago. So please consider this a question rather than some report.

I'm trying to get the axilxbar running for a testbench simulated with QuestaSim. It seems that processes like (axilxbar.v line 854)

always @(*)
  mrindex[M] = 0;

are never evaluated, mrindex stays all x.
If I add an initial statement setting mrindex to zero, it suddenly works.

As there is no signal read in the process, the simulator might well think that it never has to schedule it. But is that a general problem or is this a QuestaSim related issue?
Do I hit this because I only have one master?

Best regards,
emanuel

Is the OPT_NONESEL option currently the same as the multiple slaves?

Hi, first, thank you for all the content and code you publish, I've been following for a while. Right now I'm studying your crossbar code and realized that the request array has the same implementation for OPT_NONESEL and for !(OPT_NONESEL) & !(NS == 1).

I'm guessing a "nonesel slave" is missing as indicated by the comment, but is the code supposed to be duplicated this way or some difference in the actual request decoding is to be implemented?

wb2axip/rtl/addrdecode.v

Lines 124 to 161 in c36b2a8

generate if (OPT_NONESEL)
begin : NO_DEFAULT_REQUEST
// {{{
reg [NS-1:0] r_request;
// Need to create a slave to describe when nothing is selected
//
always @(*)
begin
for(iM=0; iM<NS; iM=iM+1)
r_request[iM] = i_valid && prerequest[iM];
if (!OPT_NONESEL && (NS > 1 && |prerequest[NS-1:1]))
r_request[0] = 1'b0;
end
assign request[NS-1:0] = r_request;
// }}}
end else if (NS == 1)
begin : SINGLE_SLAVE
// {{{
assign request[0] = i_valid;
// }}}
end else begin
// {{{
reg [NS-1:0] r_request;
always @(*)
begin
for(iM=0; iM<NS; iM=iM+1)
r_request[iM] = i_valid && prerequest[iM];
if (!OPT_NONESEL && (NS > 1 && |prerequest[NS-1:1]))
r_request[0] = 1'b0;
end
assign request[NS-1:0] = r_request;
// }}}
end endgenerate
// }}}

Which yosys version should I use?

Hi, All
I try make the formal verification in bench/formal with cmd

make all

I get stop with the following error when I use yosys e32cef40

sby -f skidbuffer.sby prfc
SBY 20:21:26 [skidbuffer_prfc] Removing direcory 'skidbuffer_prfc'.
SBY 20:21:26 [skidbuffer_prfc] Copy '../../rtl/skidbuffer.v' to 'skidbuffer_prfc/src/skidbuffer.v'.
SBY 20:21:26 [skidbuffer_prfc] engine_0: smtbmc
SBY 20:21:26 [skidbuffer_prfc] base: starting process "cd skidbuffer_prfc/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 20:21:26 [skidbuffer_prfc] base: skidbuffer.v:452: ERROR: Identifier `\default' is implicitly declared and `default_nettype is set to none.
SBY 20:21:26 [skidbuffer_prfc] base: finished (returncode=1)
SBY 20:21:26 [skidbuffer_prfc] base: job failed. ERROR.
SBY 20:21:26 [skidbuffer_prfc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 20:21:26 [skidbuffer_prfc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 20:21:26 [skidbuffer_prfc] DONE (ERROR, rc=16)
Makefile:721: recipe for target 'skidbuffer_prfc/PASS' failed
make: *** [skidbuffer_prfc/PASS] Error 16

But when I upgrade to yosys-0.9, I get

sby -f sfifo.sby prf
SBY 20:37:12 [sfifo_prf] Removing directory 'sfifo_prf'.
SBY 20:37:12 [sfifo_prf] Copy '../../rtl/sfifo.v' to 'sfifo_prf/src/sfifo.v'.
SBY 20:37:12 [sfifo_prf] engine_0: smtbmc
SBY 20:37:12 [sfifo_prf] base: starting process "cd sfifo_prf/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 20:37:12 [sfifo_prf] base: finished (returncode=0)
SBY 20:37:12 [sfifo_prf] smt2: starting process "cd sfifo_prf/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 20:37:12 [sfifo_prf] smt2: ERROR: No such command: dffunmap (type 'help' for a command overview)
SBY 20:37:12 [sfifo_prf] smt2: finished (returncode=1)
SBY 20:37:12 [sfifo_prf] smt2: job failed. ERROR.
SBY 20:37:12 [sfifo_prf] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 20:37:12 [sfifo_prf] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 20:37:12 [sfifo_prf] DONE (ERROR, rc=16)
SBY 20:37:12 One or more tasks produced a non-zero return code.
Makefile:682: recipe for target 'sfifo_prf/PASS' failed
make: *** [sfifo_prf/PASS] Error 16

skid buffer proved by smtbmc but fail by abc pdr

Hi, Dan

I try to use the formal assertion you mention in your blog and prove an other skid buffer from Altera(Intel) on github

Then I get a induction fail with smtbmc engine, it fails at Rule #3: After the last transaction, valid_o should become idle
The trace_induct.vcd give a fail trace which seems start with an impossible initial state. backup_valid would never valid when there is no valid_o and valid_i.
ready_skid_fail
But when I change the engine to abc pdr, it PASS.

I have no idea why different proof engine gets different result, could you help explain that?

Attached ready_skid.v with formal property and .sby file
BTW, I mask Rule #1 since this skid buffer has a different reset behavior

// Copyright 2008 Altera Corporation. All rights reserved.  
// Altera products are protected under numerous U.S. and foreign patents, 
// maskwork rights, copyrights and other intellectual property laws.  
//
// This reference design file, and your use thereof, is subject to and governed
// by the terms and conditions of the applicable Altera Reference Design 
// License Agreement (either as signed by you or found at www.altera.com).  By
// using this reference design file, you indicate your acceptance of such terms
// and conditions between you and Altera Corporation.  In the event that you do
// not agree with such terms and conditions, you may not use the reference 
// design file and please promptly destroy any copies you have made.
//
// This reference design file is being provided on an "as-is" basis and as an 
// accommodation and therefore all warranties, representations or guarantees of 
// any kind (whether express, implied or statutory) including, without 
// limitation, warranties of merchantability, non-infringement, or fitness for
// a particular purpose, are specifically disclaimed.  By making this reference
// design file available, Altera expressly does not recommend, suggest or 
// require that this reference design file be used in combination with any 
// other product not provided by Altera.
/////////////////////////////////////////////////////////////////////////////

// baeckler - 11-06-2008
// pipeline for ready / valid data

module ready_skid #(
	parameter WIDTH = 16
)
(
	input clk,arst,
	
	input valid_i,
	input [WIDTH-1:0] dat_i,
	output reg ready_i,
	
	output reg valid_o,
	output reg [WIDTH-1:0] dat_o,
	input ready_o	
);

reg [WIDTH-1:0] backup_storage;
reg backup_valid;

// duplicate control registers to mitigate
// high fanout loading.
reg internal_valid_o /* synthesis preserve */;
reg internal_ready_i /* synthesis preserve */;

`ifndef FORMAL
// simulation only sanity check
always @(posedge clk) begin
	if ((ready_i != internal_ready_i) || 
		(valid_o != internal_valid_o)) begin
		$display ("Error: Duplicate internal regs out of sync");	
	end
end
`else
always @(posedge clk) begin
    assert(ready_i == internal_ready_i);
    assert(valid_o == internal_valid_o);
end
`endif

always @(posedge clk or posedge arst) begin
	if (arst) begin
		ready_i <= 1'b0;
		internal_ready_i <= 1'b0;
		valid_o <= 1'b0;
		internal_valid_o <= 1'b0;
		dat_o <= 0;
		backup_storage <= 0;
		backup_valid <= 1'b0;
	end
	else begin
		ready_i <= ready_o;
		internal_ready_i <= ready_o;
		
		if (internal_valid_o & ready_o) begin
			// main data is leaving to the sink
			if (backup_valid) begin
				// dump the backup word to main storage
				backup_valid <= 1'b0;
				dat_o <= backup_storage;
				valid_o <= 1'b1;	
				internal_valid_o <= 1'b1;	
				if (ready_i && valid_i) begin
					$display ("ERROR: data lost in skid buffer");
				end
			end
			else begin
				// if not overwritten below, you are done.
				valid_o <= 1'b0;
				internal_valid_o <= 1'b0;
			end
		end
		
		if (internal_ready_i && valid_i) begin
			// must accept data from source
			if (ready_o || !internal_valid_o) begin
				// accept to main registers
				valid_o <= 1'b1;
				internal_valid_o <= 1'b1;
				dat_o <= dat_i;
			end
			else begin
				// accept to backup storage
				backup_valid <= 1'b1;
				backup_storage <= dat_i;
				ready_i <= 1'b0; // stop stop!
				internal_ready_i <= 1'b0;
			end
		end			
	end
end

`ifdef FORMAL
	reg	f_past_valid;

	initial	f_past_valid = 0;
	always @(posedge clk)
		f_past_valid <= 1;

	always @(*)
	if (!f_past_valid)
		assume(arst);
	
    ////////////////////////////////////////////////////////////////////////
	// Incoming stream properties / assumptions
	////////////////////////////////////////////////////////////////////////
	//
	always @(posedge clk)
	if (!f_past_valid) begin
		assume property(!valid_i);
    end else if ($past(valid_i && !ready_i && !arst) && !arst) begin
	    assume property(valid_i && $stable(dat_i));
    end
	
    ////////////////////////////////////////////////////////////////////////
	// Outgoing stream properties / assumptions
	////////////////////////////////////////////////////////////////////////
	//
    always @(posedge clk)
        if (!f_past_valid) begin
            // Following any reset, valid must be deasserted
            assert property(!valid_o);
        end else if ($past(valid_o && !ready_o && !arst) && !arst) begin
            // Following any stall, valid must remain high and
            // data must be preserved
            assert property(valid_o && $stable(dat_o));
        end

	////////////////////////////////////////////////////////////////////////
	// Other properties
	////////////////////////////////////////////////////////////////////////
	//
    // Rule #1:
    //	If registered, then following any reset we should be
    //	ready for a new request
//    always @(posedge clk)
//        if (f_past_valid && $past(arst))
//            prf_rst_rdy: assert property(ready_i);

    // Rule #2:
    //	All incoming data must either go directly to the
    //	output port, or into the skid buffer
    always @(posedge clk)
        if(f_past_valid && !arst && !$past(arst) && $past(valid_i && ready_i && valid_o && !ready_o))
            prf_dat: assert(!ready_i && backup_storage == $past(dat_i));

    // Rule #3:
    //	After the last transaction, valid_o should become idle
    always @(posedge clk)
        if (f_past_valid && !arst && !$past(arst)) begin
            if ($past(valid_i && ready_i))
                assert(valid_o);

            if ($past(!valid_i && ready_i && ready_o))
                assert(!valid_o);
        end

    // Rule #4
    //	Same thing, but this time for ready_i
	always @(posedge clk)
		if (f_past_valid && !arst && $past(!arst && !ready_i && ready_o))
			prf_rdy: assert property(ready_i);


`endif

endmodule
[tasks]
prf     prf
cvr     cvr
bmc     bmc

[options]
prf: mode prove
prf: depth 12

cvr: mode cover
cvr: depth 20

bmc: mode bmc
bmc: depth 20

[engines]
prf: smtbmc
prf: abc pdr

[script]
read -formal ready_skid.v
--pycode-begin--
cmd = "hierarchy -top ready_skid"
output(cmd);
--pycode-end--
prep -top ready_skid

[files]
ready_skid.v

`default_nettype none

`default_nettype none

causes real problems with Vivado, one workaround is to add "wire" in many places, but that's a real dirty workaround

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.