In short: randcase picks one branch at random using weights: each branch weight divided by the sum of all weights is its chance of being taken. randsequence is bigger; it builds structured sequences from named productions, so it can produce ordered or branching stimulus such as instruction streams. Use randcase for a quick weighted choice…
In short: Both @(e) and wait(e.triggered) pause a process until event e fires, but they treat timing differently. @(e) is edge-sensitive: the process must already be blocked on it before the trigger, or it misses the event. wait(e.triggered) is level-sensitive within the current time step: it still catches the event even if the trigger happened…
In short: The dist keyword in a constraint makes some random values appear more often than others. Two operators set the weights. := gives the stated weight to each value in a range, so a wider range gets more total probability. :/ gives the stated weight to the range as a whole, split evenly across…
In short: Directed testing writes one test per scenario you already know about. Constrained random verification (CRV) lets the simulator generate many legal, varied scenarios from a small set of rules, so it also finds bugs nobody thought to look for. Most real projects use both: CRV first to cover wide ground and catch corner…