Initial questions about getting started with a new core

[aignacio]

Hi Clifford,
first thank you for this project, seems a really good way to handle new open source designs as the community grows!. So, I'm trying to get started with it inserting the RVFI in my core but I have some simple questions due to briefly understand that are:

1. How you should write the code segment like *_FAIRNESS macros, is this something to emulate memory behavior?
2. Is there some doc related how can I configure the numbers inside checks.cfg in depth segment?
   like:

insn              20
reg       15    30

I understand that it refers to cycles of test but why some times you have 2 ou even 3 numbers defined at....should be something like:
type_of_checking reset_cycles trigger_cycle checker_cycle
?
I know that are quite basic things due to the project but it's not so close to me how to setup it.
Best regards, Anderson

[cliffordwolf]

Hi,

sorry for the late reply.

How you should write the code segment like *_FAIRNESS macros, is this something to emulate memory behavior?

Yes. Usually you would do that in form of assumptions in your rvfi_wrapper module. The assumptions should make sure that you memory model can not stall the core indefinitely by not replying to a request.

For example in rvfi_wrapper for PicoRV32:

`ifdef PICORV32_FAIRNESS
	reg [2:0] mem_wait = 0;
	always @(posedge clock) begin
		mem_wait <= {mem_wait, mem_valid && !mem_ready};
		restrict(~mem_wait || trap);
	end
`endif

Is there some doc related how can I configure the numbers inside checks.cfg in depth segment?

Unfortunately there's not documentation for the .cfg format yet. (PRs are welcome. :)

The last number is always the depth of the formal check. Setting this to a larger number will create checks with deeper bounds that will run for longer.

Some checks have a "start cycle" in which they start enabling a monitor. Setting this to a smaller number will increase the time period the monitor is running, creating a better check, but one that also runs for more time.

A few checks have a third number between start and depth. That's the "trigger". This is for checks where an event must be consistent with something that can either happen earlier or later. In that case the event is assumed to happen at the "trigger" cycle, and the correlated event can happen anywhere within the start..depth span.

I hope that helps.

[aignacio]

Hi Clifford,
thanks for replying back and for clarify with the explanations, I also talked with Tom some weeks ago to understand better about formal verification, this concepts was quite new for me that's why the questions raised, so the only methodology that I've saw in the past was UVM verification way and the amount of work/effort to make it happen was not so productive but formal way makes me rethink about having those cover+assumptions+assertions embedded in every design what quite ok.