openrisc / mor1kx

mor1kx - an OpenRISC 1000 processor IP core
Other
490 stars 146 forks source link

formal: Update ALU serial operations to time until complete #131

Closed stffrdhrn closed 3 years ago

stffrdhrn commented 3 years ago

The previous verification logic counted the cycles it took to run a multipy operation stopping when it reached 30. then confirming we were done. The new logic is a bit more flexible and simple we count until the operation is complete. If the count goes above 32 we fail. This can be used for any multi clock multiply operation so we use for 3 stage as well.

In the .sby file I have updated depth to 64 to allow k-indection to capture a valid start of a multiply operation. Also, I have changed task names to be a bit more descriptive.

stffrdhrn commented 3 years ago

I converted the multiclock check to a module so we can reuse the logic. Also the CPU level checks are fixed.

stffrdhrn commented 3 years ago

I squashed some changes and rebased it on master after merging the formal-CI PR.

Harshitha172000 commented 3 years ago

We can merge this PR for now, and can check cpu test after adding input assumptions to mor1kx_cpu_cappuccino.