Hi, I am trying to do a formal verification on ISA of the processor and I found some problems. Can I know where/whom can I report problems or can place my doubts regarding the functionality of signals? Thank you,

Hi,

This sounds very interesting. We have been interested in more formal verification of or1200 for a while. If you find something that you want to change, or think is wrong, I would suggest that you report it as a bug at bugzilla.opencores.org. That will make it easier to follow up on the issue.

We also have mailing lists at lists.opencores.org and lists.openrisc.net, and if you are looking for quick response, most of the active developers are also available on the #opencores channel at irc.freenode.net

--
Olof Kindgren
______________________________________________
ORSoC
Website: www.orsoc.se
Email: olof.kindgren@orsoc.se
______________________________________________
FPGA, ASIC, DSP - embedded SoC design

Hi, Thank you for the suggestion. As far as the verification is concerned, i think that unless there is a clear specification of the processor or/and the people who have implemented, there always will be an ambiguity whether it is a bug or not. so i hesitate to report it as a bug. It would be better if there is a developer associated so that we can easily go through matching the specification with the design. But for OR1200 there is no specification except a preliminary draft written 10 years ago. I know all the people who are/were in the development of this project will be busy but a good specification is really needed for people who would like to verify/develop/customize this processor later.

Hi,
Can anyone please provide timescale.v and or1200_defines.v for the or1200 RTL colde in ORSOC implementation.
Regards,
Hemanth Kaja

timescale.v and or1200_defines.v are part of OR1200 code that you would have downloaded from website.
OR1200 as downloaded from SVN is compile, elab clean..
Incase you don't find all files, then plz re-download freshly..

Also, formal-verification for something like OR1200 ISA can be bit painful, as you would hv to write too many assertion, and filter out lot many violations on case-to-case basis.
However, worth giving a try..

Has someone tried constrain random verification of ISA ?

with regards, pekon

Hi pekon, thanks for the reply.. you are right.. it is painful but worth a try :) I have never tried constrained random verification since i thought it would be more complex rather than writing simple formal assertions and also less focusing on the real intent of the design. But the absence of a implementation engineer, the workload is too heavy and sometimes simply not possible to perform.

hi, I am looking at the implementation of OR1200 processor and found some things I could not understand. I hope that you guys can help me with this..
1) Why is an if_stall(comes from if stage, if.v) used in freeze signals(freeze.v)? since this says that if there is no insn in the if stage, all the stages in the pipeline freeze, which I think may not be a correct way for implementing a pipeline.
2) Why is id_freeze not asserted high when there is a data error or an illegal insn is recognized eventhough ex_freeze and wb_freeze are asserted high? Because, this would cause the id stage to process the insn and are lost until ex_freeze gets asserted to low again.