The Design Optimization And Formal Verification Of F-CX Instruction-controller

F-CX is a 32-bit high-performance processor which is an advanced Very Long Instruction Word architecture.To deal with the code expansion,we introduced the variable-length instruction set and the nonalign dispatching technique.The variable-length instruction set is implemented by compact instruction,which include 32-bit instruction format and 16-bit instruction format.The pipeline of instruction-controller is based on branch delay slot mechanism to reduce its cost.These techniques make the control mechanism become more complex and enlarge the cost of the hardware.As a result,the power consumption is increased,and the function verification becomes more difficult.This paper mainly completed the design optimization include low-power design and the formal verification based on IFV of the F-CX instruction-controller.The main work of this paper is as follows:1)Optimizing the fetch-unit and dispatch-unit's design.Based on 32-bit instruction packet,this paper introduces compact instruction packet and implement the control of fetching and dispatching for this kind of packet.Then there are three kinds of instruction,including 16-bit instruction,32-bit instruction and head instruction that describes information about every instruction of a compact packet.2)Reducing the power of the instruction-controller based on low-power technologies and estimating power by Spyglass.We mainly reduced power by clock-gating to gate unused module include SPLOOP buffer and instruction-fetching..We also decrease unnecessary transitions of sub-module and some decode-modules' input signal,and optimize impelementation of combined logic to reduce power.3)Verifying functions of the instruction-controller based on Incisive Formal Verifier.To verify fetch-unit,according to nature of functions,two properties is extracted to verify more complicated functions.To verify dispatch-unit,we design a reference model by Verilog HDL to be compared with behavior of DUT.For Interrupt and Exception unit,properties is extracted according to waveform diagrams.Finally,we fine some bugs which is miss by simulate verification.