Better Randomizing Constrained Random. Innovation in Verification

Constrained random methods in simulation are universally popular, still can the method be improved? Paul Cunningham (Senior VP/GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and now Silvaco CTO) and I continue our series on research ideas. As always, feedback welcome.

The Innovation

This month’s pick is Balancing Scalability and Uniformity in SAT Witness Generator. A refined version of the paper was published by Springer in 2015 in “Proceedings of the 21^st International Conference on Tools and Algorithms for the Constructions and Analysis of Systems”. The authors are/were from IIT Bombay and Rice University, Houston TX.

Constrained random effectiveness depends on the quality of constraints, also the uniformity of the distribution generated against those constraints since uneven distributions will bias away from triggering bugs in lightly covered states. Unfortunately generation methods tend either to high uniformity but impractical run-times for large designs or to good scalability but weak uniformity. The authors’ paper describes a method to provide approximate guarantees of uniformity with better performance than prior papers on the topic.

The authors also reported a refinement to this method in a later publication apparently only available from Springer-Verlag.

Paul’s view

A key engine at the heart of all commercial logic simulators is the constraint solver, responsible for picking pseudo-random input values each clock cycle in a constrained-random test. These solvers must be ultra-fast but also pick a good spread of random values across the solution space of the constraints. For the scale of constraint complexity in modern commercial SOC tests this is a really hard problem and EDA vendors have a lot of secret sauce in their solvers to tackle it.

Under the hood of these solvers, constraints are munged into Boolean expressions, and constraint solving turns into a Boolean SAT problem. In formal verification we are trying to find just one solution to a massive Boolean expression. In constrained-random simulation we are trying to find a massive number of “uniformly distributed” solutions to smaller Boolean expressions.

The way solvers achieve uniformity is conceptually simple: partition the set of all solutions into n groups of roughly equal size, first pick a random group and then find a solution that belongs to that group. This forces the solver to spread its solutions over all the groups, and hence over the solution space. Implementing this concept is super hard and involves ANDing the Boolean expression to be solved with a nasty XOR-based Boolean expression encoding a special kind of hash function. This hash function algebraically partitions the solution space into the desired number of groups. The smaller the groups (i.e. the larger n is) the more uniform the solver, but the slower the solver is, so picking the right number of groups is not easy and must be done iteratively.

There are two key innovations in this paper: one relates to dramatically reducing the size of the XOR hash function expression, the other to dramatically reducing the number of iterations required to get the right group size. Both innovations come with rigorous proofs that the solver still meets a formal definition of being “uniform”. It’s impressive work and way too complex to explain fully here, but the results are literally 1000x faster than prior work. If you have the energy to muscle through this paper it is well worth it!

Raúl’s view

A “SAT witness” is a satisfying assignment of truth values to variables such that a Boolean formula F evaluates to true. Constraints in Constrained Random Verification (CRV) of digital circuits are encodable as Boolean formulae, so generation of SAT witnesses is essential for CRV. Since the distribution of errors in a design is not known a priori, all solutions to the constraints are equally likely to discover a bug. Hence it is important to sample the solution space uniformly at random, meaning that if there are R_F SAT witnesses, the probability P_R of generating a value is 1/R_F; the paper uses “almost” uniformly defined as 1/(1+ℇ)R_F ≤ P_R ≤ (1+ ℇ)/R_F. Uniformity poses significant technical challenges when scaling to large problem sizes. At the time of publication of the paper (2014) the proposed algorithm, UniGen, was the first to provide guarantees of almost-uniformity and scaling to hundreds of thousands of variables.  The algorithm is based on 3-independent hash-functions and it is beyond the scope of this blog to delve into it; the reader is referred to section 4 in the paper.

The experimental results show that for problems with up to 486,193 variables witnesses can be generated in less than 782 secs with a probability of 0.98 of success. Comparisons with UniWit, the state-of-the-art at the time, show runtimes that are 2-3 orders of magnitude lower. UniGen manages all 12 examples, while UniWit only can complete 7 out of 12. Uniformity is shown by comparing UniGen to a uniform sampler that simply picks solutions out of R_F randomly (Figure 1).

The industry has been moving towards increased automation and advanced verification methodologies, making commercial CRV tools more prevalent, particularly for complex digital designs. Constraint solving techniques have been a fundamental part of CRV. Recent advances have focused on improving constraint solving algorithms, optimizing random test generation, and addressing scalability challenges. And although much progress has been achieved since 2014, the reviewed paper (cited 81 times) is an excellent example that illustrates these advances.

Also Read:

Tensilica Processor Cores Enable Sensor Fusion For Robust Perception

Deep Learning for Fault Localization. Innovation in Verification

US giant swoops for British chipmaker months after Chinese sale blocked on national security grounds