search

SymbioticEDA / riscv-formal

RISC-V Formal Verification Framework
ISC License
572 stars 94 forks source link

Failed Checks in picorv32 Verification Following Quickstart Guide #36

Open myrealname opened 4 years ago

myrealname commented 4 years ago

Took a clean clone of the repo. Followed the quickstart guide to get going. Unfortunately the verification of the picorv32 results in two failed checks; csrw_mcycle_ch0 & csrw_minstret_ch0. While the quickstart guide doesn't indicate that the picorv32 should pass all of the checks, I have assumed that would be the case. I have pasted the logfile output below, of the mcycle check:

SBY 21:34:50 [csrw_mcycle_ch0] engine_0: smtbmc boolector
SBY 21:34:50 [csrw_mcycle_ch0] base: starting process "cd csrw_mcycle_ch0/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 21:34:53 [csrw_mcycle_ch0] base: finished (returncode=0)
SBY 21:34:53 [csrw_mcycle_ch0] smt2: starting process "cd csrw_mcycle_ch0/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 21:34:53 [csrw_mcycle_ch0] smt2: finished (returncode=0)
SBY 21:34:53 [csrw_mcycle_ch0] engine_0: starting process "cd csrw_mcycle_ch0; yosys-smtbmc -s boolector --presat --unroll --vlogtb-top wrapper.uut --noprogress -t 30:31 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 21:34:53 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Solver: boolector
SBY 21:34:53 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 0..
SBY 21:34:53 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 1..
SBY 21:34:53 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 2..
SBY 21:34:53 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 3..
SBY 21:34:53 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 4..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 5..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 6..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 7..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 8..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 9..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:00  Skipping step 10..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 11..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 12..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 13..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 14..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 15..
SBY 21:34:54 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 16..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 17..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 18..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 19..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 20..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:01  Skipping step 21..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 22..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 23..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 24..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 25..
SBY 21:34:55 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 26..
SBY 21:34:56 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 27..
SBY 21:34:56 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 28..
SBY 21:34:56 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Skipping step 29..
SBY 21:34:56 [csrw_mcycle_ch0] engine_0: ##   0:00:02  Checking assumptions in step 30..
SBY 21:34:58 [csrw_mcycle_ch0] engine_0: ##   0:00:05  Assumptions are unsatisfiable!
SBY 21:34:58 [csrw_mcycle_ch0] engine_0: ##   0:00:05  Status: PREUNSAT
SBY 21:34:58 [csrw_mcycle_ch0] engine_0: finished (returncode=1)
SBY 21:34:58 [csrw_mcycle_ch0] engine_0: Status returned by engine: ERROR
SBY 21:34:58 [csrw_mcycle_ch0] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:08 (8)
SBY 21:34:58 [csrw_mcycle_ch0] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:08 (8)
SBY 21:34:58 [csrw_mcycle_ch0] summary: engine_0 (smtbmc boolector) returned ERROR
SBY 21:34:58 [csrw_mcycle_ch0] DONE (ERROR, rc=16)

Did I miss something? Is there something missing in the instructions? Or is it something else entirely?

Thanks in advance, for any help.

ghost commented 4 years ago

Is there any update on this?

I also tried running the quickstart of picorv32 and csrw_mcycle_ch0, csrw_minstret_ch0 and insn_c_xor_ch0 failed.

DonaldKellett commented 4 years ago

I also got an error for csrw_mcycle_ch0 and csrw_minstret_ch0 upon building the quickstart example with no modifications as of 09/07/2020, please see attached the output log from make.

DonaldKellett commented 4 years ago

Looking at the output logs included by @myrealname and me, it seems that all the errors are caused by unsatisfiable assumptions (Status: PREUNSAT). I've looked at the SymbiYosys documentation and section 2.3.1 mentions that the --nopresat flag can be passed to sby to skip that check. I'll take a look at where sby is invoked in the framework and perhaps submit a pull request with the fix sometime, since I don't see a problem with contradictory assumptions - that would simply mean that the specification is vacuously satisfied.