Conquering the scheduling alternative explosion problem of SystemC symbolic simulation

Due to the non-determinism of the SystemC scheduler, SystemC symbolic simulation faces a scalability issue. The issue stems from enumerating all scheduling alternatives such that all design behaviors can be captured assuredly. To conquer the scheduling alternative explosion problem, we first adopt symbolic partial order reduction to reduce the equivalent scheduling alternatives for exploration. Moreover, for those scheduling alternatives that cannot be reduced by partial order reduction, we merge their execution paths (and also states) into fewer ones to prevent the number of paths from explosion. The experimental results show that we achieve a tremendous scalability improvement by combining these two techniques together.