METHOD OF AND APPARATUS FOR, AND PROGRAM FOR VERIFYING EQUIVALENCE BETWEEN BEHAVIORAL DESCRIPTION AND REGISTER TRANSFER LEVEL DESCRIPTION

For deriving an RTL description through several steps from a behavioral description, a behavioral synthesis device outputs an associated relation between intermediate level descriptions subsequent to the respective steps and intermediate level descriptions prior to the respective steps. A model extracting device extracts a model capable of expressing a control structure based on a finite state machine and an update of a signal from the behavioral description, each of the intermediate level descriptions, and the RTL description, as a model corresponding to those descriptions. A signal value function extracting device extracts signal value functions from the model. A function equivalence comparing device checks the equivalence between signal value functions prior and subsequent to the steps of the behavioral synthesis device.