NEXT (Formally Synthesised Bus Monitor)
ABD - The alternative: Simulation
The alternative is extensive simulation with overnight testing for regressions.
Can either write a RTL or ESL yes/no automaton as part of the test bench.
outputs to file and diff against golden with PERL script.
Downfall of simulation: it's non-exhaustive and time consuming.
ABD benefits (and challenges):
- Completeness (how to define this?)
- Scalability (tools limited in practice?),
- Rare corner situations (unusual conjunctions of events) are covered.
- are needed for performance analysis and general design confidence,
- can generate some production test vectors.
- can be partly formal: using bus monitors for dynamic validation and Specman/VERA constrained pattern generators for stimulus.