| 摘要 |
PROBLEM TO BE SOLVED: To thoroughly and efficiently verify equivalency between operation level descriptions and register transfer level (RTL) descriptions that are inputs into and outputs from an operation synthesis device respectively. SOLUTION: When deriving RTL descriptions from operation level descriptions through several steps, the operation synthesis device 2 outputs intermediate descriptions before and after each step and correspondences between the descriptions before and after each step. A model extraction device 5 extracts models representing control structures and signal updates based on a finite state machine as corresponding models from the operation level descriptions, intermediate level descriptions and RTL descriptions. A signal value function extraction device 7 extracts signal value functions from the models. A function equivalency comparison device 9 checks for equivalency of the signal value functions before and after each step of operation synthesis. COPYRIGHT: (C)2008,JPO&INPIT
|
