This work presents some techniques and algorithms to support teaching of logic design and computer organization through developing a web based virtual laboratory (COLDVL) and a formal verification method of bit-level equivalence checking for automatic evaluation of student designs. At the heart of the virtual laboratory is the COLDVL tool equipped with a circuit drawing and experimentation interface as a front end, a logic simulator as the back end with features to provide real laboratory like learning experience and a set of pre-designed guided experiments with the facility to add new experiments. In the front end of the tool, a repertoire of components and design functionalities for building circuits are made available. Features to aid learning include the Huffman structure identification in a circuit, detection of possible race around condition prior to simulation, automatic generation of controller unit from a given control state chart to be used in a circuit in association with a data path and a case based analysis for determining indeterminate signal values of some nets in gate level memory elements after regular round of simulation. Creation and reuse of user-defined encapsulated hierarchical modules, structural verilog netlist generation and saving user circuits with unique identification to check plagiarism are also supported. While circuit simulation is generally carried out in an event driven manner, a more efficient simulation technique has been devised for circuits conforming to the Huffman model. Laboratory experiments using COLDVL are conveniently conducted on a regular desktop or laptop computer.

Automated checking of student assignments through application of formal verification is a novel feature of this work. A new bit-level equivalence checking method has been developed for this purpose to compare the designs submitted by students against a reference design provided by the instructor. A submitted design may differ from the reference design in non-trivial ways but may still be perfectly acceptable. The aim of the equivalence checker is to determine conformance to the reference design despite the differences. Bit-level arithmetic, logical and shifting operations, conditional branching, etc. are handled along with computer arithmetic algorithms (eg. multiplication and division) that build the result through stages involving shifting.

The developed virtual laboratory has been successfully used in undergraduate and postgraduate laboratory courses in IIT Kharagpur.