The present invention relates to a system for verifying the proper operation of a digital logic circuit and program product therefore. In order to add a useful alternative in the field of functional, exhaustive simulation and of symbolic simulation, it is proposed to perform the steps of: a) marking a net with an additional property other than a bit value, wherein both said bit value and said additional property are valid at said net at a given time; b) propagating the marking of the net according to a set of predetermined semantic rules, wherein the set of predetermined semantic rules are defined according to a predetermined simulation; and c) generating an output at a predetermined downstream location of the digital logic circuit, said output providing an information, if or if not said property has propagated through the circuit to said predetermined downstream location or not.