HOME       UP       PREV       NEXT (ABD - Boolean Equivalence Checker)  

ABD - Creative use of a simple Model Checker

If we simulate the circuit above we have to provide stimulus for the input data and push and pop command inputs.

The harness built around the LIFO has a `floating' input that would also need a stimulus waveform in a simulation. It checks that the word pushed first after its first +ve transition comes out again at the correct time.

A simple state-based model checker tool applied to the above system will check correct operation for all words in and out even though only one holding register is present in the harness. (Thanks to Daryl Stewart of ARM for teaching this technique.)

Cadence JasperGold is commonly used in industry.


25: (C) 2012-17, DJ Greaves, University of Cambridge, Computer Laboratory.