Simulation Based Verification using Temporally Attributed Boolean Logic

We propose a specification logic called temporally attributed Boolean (TAB) logic for assertion based verification which allows us to: (i) represent assertions succinctly, (ii) incorporate data-orientation and (iii) associate timing in design intentions. We present examples to show the motivation for this logic especially in the context of high level modeling of complex real time systems. We formally define TAB logic, formulate the problem of verification on a simulation trace and present efficient algorithms to check TAB assertions. We present results of application of TAB logic for instruction semantics and bus transaction verification of a bus integrated pipelined processor implementation