HOME       UP       PREV       FURTHER NOTES       NEXT (ABD - Sequential Logic Equivalence)  

ABD - Model Checking a FIFO Queue and LIFO Stack

images/lifo-modelcheck.png

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.) The condition for checking is that never does the fail output hold.


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