{"id":10137,"date":"2018-08-14T11:48:48","date_gmt":"2018-08-14T11:48:48","guid":{"rendered":"https:\/\/www.techdesignforums.com\/practice\/?p=10137"},"modified":"2018-08-20T17:42:41","modified_gmt":"2018-08-20T17:42:41","slug":"doc-formal-achieving-exhaustive-formal-verification-of-packet-based-designs","status":"publish","type":"post","link":"https:\/\/www.techdesignforums.com\/practice\/technique\/doc-formal-achieving-exhaustive-formal-verification-of-packet-based-designs\/","title":{"rendered":"Doc Formal: Achieving exhaustive formal verification of packet-based designs"},"content":{"rendered":"

The verification of designs that transport data in a serial manner is a challenge for both simulation and formal techniques. The complexity of such designs stems from the \u2018serialized\u2019 nature of the packet flow where the state of each packet depends upon the history of all the previous packets in flight. What is interesting about such designs is that they are present everywhere in all kinds of hardware designs. Packet-based serialized data flows can be seen in networking routers, bus protocols, bus bridges, load-store units in CPUs, packing and unpacking designs, and SoC peripherals such as I2<\/sup>C, I2<\/sup>S, USB, UART, Ethernet.<\/p>\n

These designs are inherently complex with multiple mutually interacting state machines. At a high level they are about data flow but the control mesh that routes the data correctly can be very difficult to verify completely with directed testing or by constrained random simulation. If you throw in this mix the fact that you can have multiple clock domains \u2013 one for the input and the other for the output – obtaining a near exhaustive result is nearly impossible. Nevertheless, while the formal verification of such designs is a challenging task, it can be solved through a combination of methodology and technology.<\/p>\n

When methodology meets technology<\/h3>\n

I have used many formal tools over the past 20 years and seen the underlying technology evolve. Existing tools have improved and new players have come in to the field.<\/p>\n

Axiomise<\/strong><\/a> recently became a Synopsys<\/strong><\/a> partner. I was keen to lay my hands-on VC Formal<\/strong><\/a>, one of its more recent tools. At its heart VC Formal is a model checker (a.k.a. property checker) with a suite of applications (apps) stacked on top. I wanted to focus on property checking and wanted to see how the tool coped with the design example discussed in the introduction. I was impressed by the overall quality of VC Formal and its feature-rich offering for both novice and advanced users. Not only was the tool able to find bugs in my design (which I introduced) but it was also able to converge on proofs on hard sequential properties, helped by the Axiomise methodology on scalable formal proofs. I like the fact that the VC Formal orchestration layer enables a wide variety of proof engines to co-operate amongst themselves to speed up their work once sufficient proof engineering support is provided by the user.<\/p>\n

Coping with formal complexity<\/span><\/h3>\n

Abstraction<\/strong><\/a> is one of the main recipes to control the complexity of formal verification so that we not only find deep bugs in such designs but also obtain exhaustive proofs.<\/p>\n

I haveve been pursuing research and application of abstraction for scalable formal verification for 17 years – starting in the early days with my doctoral thesis<\/strong><\/a>\u00a0in problem reduction techniques for scalable model checking.<\/p>\n

Let\u2019s look at some of the published literature on this topic. Ed Clarke\u2019s paper<\/strong><\/a> is a great read and addresses abstraction techniques nicely. I have also found that, especially on serial designs, a combination of data and temporal abstraction techniques works very well in practice, and this approach dates back to the foundational work<\/strong><\/a> done by Tom Melham. Though a lot of early work done by Melham\u00a0was in the context of theorem proving and higher order logic, the application of these concepts is highly relevant to model checking as well \u2013 and this is what has inspired me to build my own abstraction-based solutions.<\/p>\n

Smart tracker abstraction<\/span><\/h3>\n

To verify any data transport design, the testbench must observe all the necessary data flows. This is typically done in simulation by tracking all the concrete traces of data words comprising 0s and 1s. All data is tracked at all clock cycles in a scoreboard and at the output the data is compared to what is supposed to be the expected value sampled at the input side.<\/p>\n

The key idea in smart tracker abstraction is that we do not explicitly track all the data; we track only one data value. However, that data word is non-deterministically chosen by the formal tool at runtime. The formal tool will instantiate all possible data values to this non-deterministic variable; the user does not have to do anything. This contrasts with simulation where the stimulus is explicitly applied and manipulated.<\/p>\n

In our discussion, we will call the non-deterministic variable a \u2018watched value\u2019. We use a counter to track the watched value.<\/em> On a new data write when a new word is accepted in the DUT, this counter increments, and continues to increment until the watched data appears on the input port. On every read, when the data is read out the counter decrements. When the counter reaches the value one, we expect to see the watched value on the output. If we see any other data appear at the output \u2013 due, say, to a design bug such as reordering, data loss, or duplication – we will detect the bug as the output data will not match the watched data.<\/p>\n

We used this approach to verify a family of FIFOs and noted a massive performance boost. We exhaustively verified FIFOs as deeps as 8192 carrying 32-bit payloads using this abstraction. Though our packet design, and the numerous other serial designs were an order of magnitude more complex than FIFO implementations, the basic transaction counting method rooted in smart tracker abstraction was effectively the main vehicle behind the exhaustive verification of such designs.<\/p>\n

The reason this tracker is called \u2018smart\u2019 is because it only tracks one symbolic data value and yet tracks all the data values in the design. Moreover, due to the data independence nature of data transport designs, we do not need to observe, store or compare other data values entering and exiting the DUT. By not doing explicit observation, storage or comparison of other values, we save compute time and memory.<\/p>\n

We carried out comparisons of the smart tracker method with the two-transaction method where one tracks two distinct values. We found that smart tracker method outperforms the two-transaction method in compute speed, scalability and time. We discuss these techniques in detail in the Axiomise formal verification training<\/strong><\/a> program.<\/p>\n

Serial packet design<\/span><\/h3>\n

Our packet-based design has three dimensions. The first dimension is the depth of the buffer (Figure 1 shows an 8-deep buffer). Each buffer location can have a varying number of packets and the maximum number that can be stored is configured to be a fixed number at run time. The buffer depth\u00a0is controlled through a parameter as well. The packets themselves can be of any size ranging from 1 bit to n<\/em>-bits also configured and fixed at run time. Figure 1 shows a layout where we have an 8-deep buffer with each buffer location able to store up to four packets, each packet being of 8-bit. The green dots indicate how many of the packet locations are harvested so far by active packets. Buffer location 0 has four active packets, while buffer location 1 has one, and so on.<\/p>\n

\"Figure<\/a>

Figure 1: An example of a packet-based design layout (Axiomise)<\/p><\/div>\n

Figure 2 shows the design interface. Input data is transferred in packets where each input packet is written into data_i<\/strong>\u00a0on an input handshake hsk_i<\/strong>\u00a0(valid_i && enable_o<\/strong>). Output data is read out on an output handshake hsk_o<\/strong>\u00a0(valid_o && enable_i<\/strong>).<\/p>\n

Exactly how many packets are written is defined by the input pkt_len<\/strong>\u00a0which is registered into the design on the very first beat of the input handshake of a new packet. Subsequent, values of pkt_len<\/strong>\u00a0(which is PKT_BITS<\/strong>\u00a0wide) are disregarded until another new packet stream is seen. The read and write of the packets is controlled by buffer read\/write FSM which is a function of read\/write pointers indexing the buffer depth and a packet read\/write FSM which is a function of packet read\/write pointers indexing the packet locations. A new valid write starts when the write pointer index is pointing to 0 and there is an input handshake. In this clock cycle, the value of pkt_len<\/strong>\u00a0is registered in the design and this is how many packets would be written at this buffer index pointed to by wptr<\/strong>. So, the wptr<\/strong>\u00a0walks along the buffer depth, while pkt_wptr<\/strong>\u00a0indexes the individual packets at a given buffer location. Similarly, rptr<\/strong>\u00a0reads along the buffer depth, while pkt_rptr<\/strong>\u00a0reads the individual packets from the buffer indexed by rptr<\/strong>. The design also has flags empty_o<\/strong>\u00a0and full_o<\/strong>\u00a0to indicate when it is empty and full respectively, and, is driven to reset by an active low resetn.<\/strong><\/p>\n

\"Figure<\/a>

Figure 2: Packet design interface (Axiomise)<\/p><\/div>\n

Verifying packet transfer<\/span><\/h3>\n

Since this is a multi-packet design, we need an array of watched values not just one.<\/p>\n

We define these watched values by using the logic datatype in SV:\u00a0logic [DATA_WIDTH-1:0] wd [PKT_LEN-1:0];\u00a0<\/strong>Here,\u00a0PKT_LEN<\/strong>\u00a0is a function of the input pkt_len<\/strong>\u00a0and is defined as 1<<PKT_BITS.<\/strong><\/p>\n

\"Figure<\/a>

Figure 3: Auxiliary logic used for transaction tracking (Axiomise – click to enlarge)<\/p><\/div>\n

We constrain these watched values to be stable after reset. This allows the formal tool to keep the values stable for each run that it executes, but the value in each run is chosen to be unique. We show four sampling registers we use for detecting the entry and exit of the watched packet stream in Figure 3.<\/p>\n

The ready_to_*_sampling_in_*<\/strong>\u00a0signals are defined in Figure 4.<\/p>\n

\"Figure<\/a>

Figure 4: Defined signals (Axiomise – click to enlarge)<\/p><\/div>\n

The sample_in_*_cond<\/strong>\u00a0signals are wires, while the sample_*_started<\/strong>\u00a0and sample_*_finished<\/strong>\u00a0signals are registers. The sample_in_started_cond<\/strong>\u00a0signal is high on an input handshake, when the packet write pointer is 0, and the very first watched data packet wd[0]<\/strong>\u00a0appears on data_i<\/strong>. The sample_in_finish_cond<\/strong>\u00a0signal is high on an input handshake, when the packet write pointer is equal to the value that is meant to be written, and we are ready to start sampling in (i.e., we had started to write the earlier packets since those conditions were met earlier).<\/p>\n

The sample_out_started_cond<\/strong>\u00a0is met when input has been sampled completely and read has been issued and the tracking counter is one. The signal sampling_out_finish_cond<\/strong>\u00a0goes high on an output handshake when the packet read pointer is equal to the value stored at the time of the packet write and earlier conditions for sampling out data have been met through ready_to_start_sampling_out<\/strong>.<\/p>\n

Two other useful signals we need to express our intent are shown in Figure 5.<\/p>\n

\"Figure<\/a>

Figure 5. Signals to express intent (Axiomise – click to enlarge)<\/p><\/div>\n

The smart tracker counter can now be defined as shown in Figure 6.<\/p>\n

\"Figure<\/a>

Figure 6. Smart tracker counter (Axiomise – click to enlarge)<\/p><\/div>\n

The related increment and decrement are shown in Figure 7. <\/strong>The signal cpkt_len<\/strong>\u00a0stores the packet size on every input write handshake.<\/p>\n

\"Figure<\/a>

Figure 7: Increment and decrement (Axiomise)<\/p><\/div>\n

We sample in the size of the packets by reading in the pkt_len<\/strong>\u00a0when the sampling condition is set which is defined by sample_in_started_cond<\/strong>. We copy this value into a register called the watched_pkt_len<\/strong>.<\/p>\n

The property that establishes that all packets received at the input interface are delivered to the output at the correct time without loss, reorder or duplication is shown in Figure 8. What we need is a property for each packet. Here, the counter_out<\/strong>\u00a0counts how many watched packets are left to come out once they have been sampled in completely but not sampled out.<\/p>\n

\"Figure<\/a>

Figure 8: Property to ensure packets at input are to delivered to output (Axiomise – click to enlarge)<\/p><\/div>\n

We use a generate loop to model these, where the loop itself is sensitive to PKT_LEN <\/strong>(Figure 9).<\/p>\n

\"Figure<\/a>

Figure 9. Loop to model packets (Axiomise – click to enlarge)<\/p><\/div>\n

Note, that the loop above ranges up to PKT_LEN-2<\/strong>, and for the final packet PKT_LEN-1<\/strong>, we write a separate assertion. This is due to the design artefact and the way we have modeled our testbench registers that track the data. For the very last packet in the cycle we read the register sample_out_finished<\/strong>\u00a0is high. When sample_out_finished<\/strong>\u00a0goes high then we see the watched data stored at index PKT_LEN-1,<\/strong> or the watched packet at location 0 is seen (for those cases where the watched packet is of length 0).<\/p>\n

The property that checks that the very last packet has been delivered is shown in Figure 10.<\/p>\n

\"Figure<\/a>

Figure 10. Property to check last packet (Axiomise – click to enlarge)<\/p><\/div>\n

Results and discussion<\/h3>\n

We carried out a range of runs using the VC Formal Property Verification (FPV) app on different configurations of buffer depth, maximum packets, and the width of the data vector. The results are shown for an 8-deep buffer in Figure 11. What we noted was that with increasing packet sizes the proof times were scaling linearly when the data width was 1-bit.<\/p>\n

\"Figure<\/a>

Figure 11: Run times for 8-deep buffer with varying packet lengths up to 32 packets (Axiomise)<\/p><\/div>\n

However, if you test the assertions for the entire word at once, this tool (or for that matter any tool) will not be able to converge in a predictable manner. So, we sliced the data word property into smaller bit-level properties and ran them sequentially to accumulate the overall run time for the entire word.<\/p>\n

Of course, one can run these in parallel with multiple CPU cores. We carried out these runs on a virtual Linux machine with 6 GB memory and a single CPU core. The Complexity Report feature in VC Formal shows that the size and depth of the buffer is a bottleneck that must be overcome.<\/p>\n

To increase the proof convergence rate on deeper configurations of the design involves stitching additional helper properties to make it easier for VC Formal to deduce the proof convergence sooner. Once we provided the helper properties, we were able to prove a configuration instance where the buffer depth was 256 with variable packet sizes of up to 8 packets carrying 32-bit data (nearly 10\u00a020,000<\/sup>\u00a0states).<\/p>\n

The Iterative Convergence Methodology (ICM) feature in VC Formal\u00a0can aid in identifying the helper properties. However, we did not use it in this case as we were familiar with what was needed.<\/p>\n

Verification of sequential designs is a challenge for all verification technologies including simulation and formal verification. But if you use the right methodology with a mature tool that has great solvers a significant boost in performance can be achieved.<\/p>\n

This topic is covered in greater depth in Axiomise training programs. More information on those is available here<\/strong><\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"

Ashish Darbari breaks down formal’s value to this challenging verification task with code examples and reference to VC Formal from Synopsys.<\/p>\n","protected":false},"author":138,"featured_media":9429,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[35],"tags":[2215,2214,2217,1040,1108,1919,2220,2216,2213,2218,891,2212,2221,2219,567,2222],"coauthors":[1441],"class_list":["post-10137","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-design-verification","tag-bus-bridges","tag-bus-protocols","tag-cpus","tag-ethernet","tag-formal-verification","tag-i2c","tag-i2s","tag-load-store-units","tag-networking-routers","tag-packing-designs","tag-soc","tag-tracker","tag-uart","tag-unpacking-designs","tag-usb","tag-vc-formal","workflow-analysis","workflow-diagnostic","workflow-expert-blog","workflow-up-to-date","organization-axiomise","organization-synopsys"],"_links":{"self":[{"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/posts\/10137","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/users\/138"}],"replies":[{"embeddable":true,"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/comments?post=10137"}],"version-history":[{"count":0,"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/posts\/10137\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/media\/9429"}],"wp:attachment":[{"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/media?parent=10137"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/categories?post=10137"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/tags?post=10137"},{"taxonomy":"author","embeddable":true,"href":"https:\/\/www.techdesignforums.com\/practice\/wp-json\/wp\/v2\/coauthors?post=10137"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}