Hello everyone, I'm student in HUST, I have a assignment about formal verification with CPU of or1200, and I feel some difficult when try to write property(by SVA) for any instruction, because I can't find information about timing diagram of CPU when implement instruction.

So I'm very thankful if you can help me to pass this obstacle, not only Or1200, any information about CPU of any OpenRisc same Or1200 also help me so much.

Thank you and best wish for you!

I would recommend you to use mor1kx instead of or1200. It is a more modern implementation that is more readable, faster and has more features.

I don't think there are any timing diagrams however for instructions for any of the OpenRISC implementations. What kind of timing diagram are you looking for? Most instructions spend one cycle in each pipeline stage unless there are any hazards, so it's pretty straightforward

//Olof