Non-Determinism (ND):<\/strong> this is a technique that uses \u201cfree variables\u201d implemented as un-driven wires or extra inputs in a checker to tell the formal engines they are free to consider any cases involving all possible values of the variables at once.<\/p>\n Taking advantage of Data Independence is as simple as reducing the width of a data path in a property, as long as the property\/assertion does NOT depend on the specific values of the data. For example, for verifying the data integrity of a FIFO, you only need to check that data written in will be read out correctly and in the right order — whether the FIFO width is 32 bits, 8 bits, or just 1 bit. A property that captures this intent is effectively data independent! Consequently, you can go ahead and reduce the width of the FIFO to 1 bit in the property code and the result of the formal analysis will still be valid.<\/p>\n Non-Determinism is about another form of freedom \u2013 the freedom not to care what a given input signal\u2019s value is a-priori. Consider the following: if the variable \u201clatency\u201d is really big, this assertion can introduce a lot of extra cycles into the analysis.<\/p>\n Fortunately, we can recode it as follows where \u201ccnt\u201d has (log2 latency) bits that reduces the number of states. We only check the latency between one \u201creq\u201d and one \u201cack\u201d, while introducing a new free variable, \u201cstart\u201d, to let formal consider all random start times for \u201creq\u201d, thus consider all \u201creq\u201d<\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n <\/p>\n Still unclear?\u00a0 The state diagram below corresponds to the ND-exploiting \u201cstart\u201d free variable:<\/p>\n As you can see, the addition of the \u201cstart\u201d signal limits the check to only one pair of \u201creq\u201d and \u201cack\u201d. However due to the non-deterministic feature of the free \u201cstart\u201d, formal considers all possibles, and the result is valid for both proof and firing.<\/p>\n Recall that assertions are essentially synthesized to logic. Hence, when the latency is 128, the logic introduced by the original assertion \u201cCheck_ack\u201d has 128 flops that are a pipeline to remember the value of \u201creq\u201d, In contrast, the logic introduced by the assertion using the ND technique only has 10 flops (2 for \u201cstate\u201d and 8 for \u201ccnt\u201d).\u00a0 Clearly, the ND version\u2019s dramatically lower flop count means the complexity for formal analysis is significantly reduced, which will directly translate to faster run times and lower memory usage.<\/p>\n Once you get the hang of applying DI and ND, before you know it you will start to see opportunities to apply these principals everywhere. Your colleagues will marvel at your formal analysis expertise as you get more and more proofs or CEXs, fast.<\/p>\n <\/p>\n We trust that the various techniques to resolve Inconclusives that we have reviewed in this six part series will make your more productive. Please let us know in the Comments below, or offline via email!<\/p>\n May your state spaces be shallow, and your analyses be conclusive!<\/p>\n Jin Hou, Joe Hupcey III <\/p>\n Reference Links:<\/strong><\/p>\n Part 1: Finding Where Formal Got Stuck and Some Initial Corrective Steps to Take<\/a><\/p>\n Part 2: Reducing the Complexity of Your Assumptions<\/a><\/p>\n Part 3: Assertion Decomposition<\/a><\/p>\n Part 4: Counter Abstraction<\/a><\/p>\n![\"\"](\"https:\/\/blogs.sw.siemens.com\/wp-content\/uploads\/sites\/54\/2018\/10\/HRTCOFA-Part-6-code-example1.jpg\")
<\/a><\/p>\n<\/p>\n<\/a><\/p>\n
\nfor the Questa Formal Team<\/p>\n