Formal verification of one-hot state machine. 
Author Message
 Formal verification of one-hot state machine.

Hi,

I'm attempting to use Chrysalis (Avanti's formal verification tool)
to verify a state machine design.  The state machine was binary
encoded in the RTL (verilog).  The synthesis tool was configured to
implement a one-host state machine.  Does anyone know how to map the
binary encoded state points in the RTL to the one-hot state points
in the gates?



Mon, 05 Jul 2004 04:05:34 GMT  
 
 [ 1 post ] 

 Relevant Pages 

1. One-Hot or Gray-Code State Machine

2. One-Hot or Gray-Code State Machine?

3. One-hot state machines

4. Output decoding of one hot encoded state machine

5. One Hot state machine encoding with Max+plus

6. BACUP meeting: Formal Verification, Physical Verification; SourceLink

7. BACUP meeting: Formal Verification, Physical Verification; SourceLink

8. acquiring data in one phase of a state machine and saving it in another

9. Help with large state machine design (62 states)

10. State Machine - State Definition Question

11. finite state machines, state cad

12. Stack machine to state machine

 

 
Powered by phpBB® Forum Software