read_systemverilog `-formal` support

ollie-etl commented 1 year ago

My appologies if i've missed this in the docs, but I'm unable to use as a front end for formal verification

This just fine: bmc, prove and cover statements all run ok

read -sv -formal dataflow_formal.sv
read -sv -formal dataflow_id.sv
prep -top dataflow_id

This does not

verilog_defines -DFORMAL=1 -USYNTHESIS
read_systemverilog -defer dataflow_formal.sv
read_systemverilog -defer dataflow_id.sv
read_systemverilog -link
prep -top dataflow_id

Specifically, it runs the checks, but it has no invarients in bmc and prove, and no cover statements are covered. Everything is marked pass. What is the preferred way to replace read with read_systemverilog for driving formal verification?

alaindargelas commented 1 year ago

@tgorochowik can you check what is missing?

rkapuscik commented 1 year ago

Thanks for your interest in this plugin! We have focused mostly on the synthesizable subset so far, so support for formal verification is incomplete.

I looked through -formal implementation in Yosys and first areas to look into are:

propagating the -formal argument and proper defines to Yosys,
support for various keywords (and check if they are not skipped as non-synthesizable in UHDM),
revisiting the systemverilog_defines feature (plugin doesn't have access to verilog_defines unfortunately)

Do you have any design that you can share as an example to test against? This would help to identify the areas to focus on.

ollie-etl commented 1 year ago

I can share the design (will post tomorrow - also happy to try and create as a test). The example here is some simple rules around a dataflow like bus (valid, ready, data), and a component which is literally a passthrough wire, with some cover statements relating to valids.

ollie-etl commented 1 year ago

@rkapuscik Here is a reduced example. I only use the verilog + some sv reduced syntax that yosys already suports. My interest here is in getting better yosys support for RTL code, with things like multi-dimensional arrays, rather than full SVA support.

ex1.sv

module ex1 (
    input  logic a,
    output logic b
);
  assign a = b;

  always_comb cover_in_eq_out : cover (a == b);
  always_comb cover_in_neq_out : cover (a != b);

  always_comb assert_a_eq_b : assert (a == b);
  always_comb assert_a_neq_b : assert (a != b);
endmodule

And the sby script ex1.sby

# See https://symbiyosys.readthedocs.io/en/latest/reference.html#
[tasks]
bmc
prove
cover

[options]
depth 2
append 1

bmc:   mode bmc
prove: mode prove
cover: mode cover

[engines]
smtbmc

[script]
# Replace `read` with `read_systemverilog`
# read -sv -formal ex1.sv
read_systemverilog ex1.sv
prep -top ex1

[files]
./ex1.sv

Extracts from read -sv -formal

SBY  8:57:53 [ex1_bmc] engine_0: smtbmc
SBY  8:57:53 [ex1_bmc] base: starting process "cd ex1_bmc/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  8:57:53 [ex1_bmc] base: finished (returncode=0)
SBY  8:57:53 [ex1_bmc] smt2: starting process "cd ex1_bmc/model; yosys -ql design_smt2.log design_smt2.ys"
SBY  8:57:53 [ex1_bmc] smt2: finished (returncode=0)
SBY  8:57:53 [ex1_bmc] engine_0: starting process "cd ex1_bmc; yosys-smtbmc --presat --unroll --noprogress -t 2  --append 1 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Solver: yices
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  BMC failed!
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Appending additional step 1.
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Re-solving with appended steps..
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Assert failed in ex1: assert_a_neq_b
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY  8:57:53 [ex1_bmc] engine_0: ##   0:00:00  Status: failed
SBY  8:57:53 [ex1_bmc] engine_0: finished (returncode=1)
SBY  8:57:53 [ex1_bmc] engine_0: Status returned by engine: FAIL
SBY  8:57:53 [ex1_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:57:53 [ex1_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:57:53 [ex1_bmc] summary: engine_0 (smtbmc) returned FAIL
SBY  8:57:53 [ex1_bmc] summary: counterexample trace: ex1_bmc/engine_0/trace.vcd
SBY  8:57:53 [ex1_bmc] DONE (FAIL, rc=2)
SBY  8:57:53 [ex1_prove] engine_0: smtbmc
SBY  8:57:53 [ex1_prove] base: starting process "cd ex1_prove/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  8:57:53 [ex1_prove] base: finished (returncode=0)
SBY  8:57:53 [ex1_prove] smt2: starting process "cd ex1_prove/model; yosys -ql design_smt2.log design_smt2.ys"
SBY  8:57:53 [ex1_prove] smt2: finished (returncode=0)
SBY  8:57:53 [ex1_prove] engine_0.basecase: starting process "cd ex1_prove; yosys-smtbmc --presat --unroll --noprogress -t 2  --append 1 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY  8:57:53 [ex1_prove] engine_0.induction: starting process "cd ex1_prove; yosys-smtbmc --presat --unroll -i --noprogress -t 2  --append 1 --dump-vcd engine_0/trace_induct.vcd --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2"
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Solver: yices
SBY  8:57:53 [ex1_prove] engine_0.induction: ##   0:00:00  Solver: yices
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Checking assumptions in step 0..
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Checking assertions in step 0..
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  BMC failed!
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Appending additional step 1.
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Re-solving with appended steps..
SBY  8:57:53 [ex1_prove] engine_0.induction: ##   0:00:00  Trying induction in step 2..
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Assert failed in ex1: assert_a_neq_b
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY  8:57:53 [ex1_prove] engine_0.induction: ##   0:00:00  Trying induction in step 1..
SBY  8:57:53 [ex1_prove] engine_0.induction: ##   0:00:00  Temporal induction successful.
SBY  8:57:53 [ex1_prove] engine_0.induction: ##   0:00:00  Status: passed
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY  8:57:53 [ex1_prove] engine_0.basecase: ##   0:00:00  Status: failed
SBY  8:57:53 [ex1_prove] engine_0.induction: finished (returncode=0)
SBY  8:57:53 [ex1_prove] engine_0: Status returned by engine for induction: pass
SBY  8:57:53 [ex1_prove] engine_0.basecase: finished (returncode=1)
SBY  8:57:53 [ex1_prove] engine_0: Status returned by engine for basecase: FAIL
SBY  8:57:53 [ex1_prove] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:57:53 [ex1_prove] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:57:53 [ex1_prove] summary: engine_0 (smtbmc) returned pass for induction
SBY  8:57:53 [ex1_prove] summary: engine_0 (smtbmc) returned FAIL for basecase
SBY  8:57:53 [ex1_prove] summary: counterexample trace: ex1_prove/engine_0/trace.vcd
SBY  8:57:53 [ex1_prove] DONE (FAIL, rc=2)
SBY  8:57:53 [ex1_cover] engine_0: smtbmc
SBY  8:57:53 [ex1_cover] base: starting process "cd ex1_cover/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  8:57:53 [ex1_cover] base: finished (returncode=0)
SBY  8:57:53 [ex1_cover] smt2: starting process "cd ex1_cover/model; yosys -ql design_smt2.log design_smt2.ys"
SBY  8:57:53 [ex1_cover] smt2: finished (returncode=0)
SBY  8:57:53 [ex1_cover] engine_0: starting process "cd ex1_cover; yosys-smtbmc --presat --unroll -c --noprogress -t 2  --append 1 --dump-vcd engine_0/trace%.vcd --dump-vlogtb engine_0/trace%_tb.v --dump-smtc engine_0/trace%.smtc model/design_smt2.smt2"
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Solver: yices
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Checking cover reachability in step 0..
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Appending additional step 1.
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Re-solving with appended steps..
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Reached cover statement at cover_in_eq_out in step 0.
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Assert failed in ex1: assert_a_neq_b (step 0)
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Assert failed in ex1: assert_a_neq_b (step 1)
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace0.vcd
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace0_tb.v
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace0.smtc
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Unreached cover statement at cover_in_neq_out.
SBY  8:57:53 [ex1_cover] engine_0: ##   0:00:00  Status: failed
SBY  8:57:53 [ex1_cover] engine_0: finished (returncode=1)
SBY  8:57:53 [ex1_cover] engine_0: Status returned by engine: FAIL
SBY  8:57:53 [ex1_cover] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:57:53 [ex1_cover] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:57:53 [ex1_cover] summary: engine_0 (smtbmc) returned FAIL
SBY  8:57:53 [ex1_cover] DONE (FAIL, rc=2)
SBY  8:57:53 The following tasks failed: ['bmc', 'prove', 'cover']

Result with read_systemverilog

SBY  8:58:05 [ex1_bmc] engine_0: smtbmc
SBY  8:58:05 [ex1_bmc] base: starting process "cd ex1_bmc/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  8:58:05 [ex1_bmc] base: [INF:CM0023] Creating log file slpp_all/surelog.log.
SBY  8:58:05 [ex1_bmc] base: [WRN:PA0205] ex1.sv:1:1: No timescale set for "ex1".
SBY  8:58:05 [ex1_bmc] base: [INF:CP0300] Compilation...
SBY  8:58:05 [ex1_bmc] base: [INF:CP0303] ex1.sv:1:1: Compile module "work@ex1".
SBY  8:58:05 [ex1_bmc] base: [INF:CP0302] Compile class "work@mailbox".
SBY  8:58:05 [ex1_bmc] base: [INF:CP0302] Compile class "work@process".
SBY  8:58:05 [ex1_bmc] base: [INF:CP0302] Compile class "work@semaphore".
SBY  8:58:05 [ex1_bmc] base: [INF:EL0526] Design Elaboration...
SBY  8:58:05 [ex1_bmc] base: [NTE:EL0503] ex1.sv:1:1: Top level module "work@ex1".
SBY  8:58:05 [ex1_bmc] base: [NTE:EL0508] Nb Top level modules: 1.
SBY  8:58:05 [ex1_bmc] base: [NTE:EL0509] Max instance depth: 1.
SBY  8:58:05 [ex1_bmc] base: [NTE:EL0510] Nb instances: 1.
SBY  8:58:05 [ex1_bmc] base: [NTE:EL0511] Nb leaf instances: 1.
SBY  8:58:05 [ex1_bmc] base: [INF:UH0706] Creating UHDM Model...
SBY  8:58:05 [ex1_bmc] base: [  FATAL] : 0
SBY  8:58:05 [ex1_bmc] base: [ SYNTAX] : 0
SBY  8:58:05 [ex1_bmc] base: [  ERROR] : 0
SBY  8:58:05 [ex1_bmc] base: [WARNING] : 1
SBY  8:58:05 [ex1_bmc] base: [   NOTE] : 5
SBY  8:58:05 [ex1_bmc] base: Warning: ex1.sv:7: Skipping non-synthesizable object of type 'immediate_cover'
SBY  8:58:05 [ex1_bmc] base: Warning: ex1.sv:8: Skipping non-synthesizable object of type 'immediate_cover'
SBY  8:58:05 [ex1_bmc] base: finished (returncode=0)
SBY  8:58:05 [ex1_bmc] smt2: starting process "cd ex1_bmc/model; yosys -ql design_smt2.log design_smt2.ys"
SBY  8:58:05 [ex1_bmc] smt2: finished (returncode=0)
SBY  8:58:05 [ex1_bmc] engine_0: starting process "cd ex1_bmc; yosys-smtbmc --presat --unroll --noprogress -t 2  --append 1 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Solver: yices
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Checking assertions in step 0..
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  BMC failed!
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Appending additional step 1.
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Re-solving with appended steps..
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Assert failed in ex1: assert_a_neq_b
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY  8:58:05 [ex1_bmc] engine_0: ##   0:00:00  Status: failed
SBY  8:58:05 [ex1_bmc] engine_0: finished (returncode=1)
SBY  8:58:05 [ex1_bmc] engine_0: Status returned by engine: FAIL
SBY  8:58:05 [ex1_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:58:05 [ex1_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:58:05 [ex1_bmc] summary: engine_0 (smtbmc) returned FAIL
SBY  8:58:05 [ex1_bmc] summary: counterexample trace: ex1_bmc/engine_0/trace.vcd
SBY  8:58:05 [ex1_bmc] DONE (FAIL, rc=2)
SBY  8:58:05 [ex1_prove] engine_0: smtbmc
SBY  8:58:05 [ex1_prove] base: starting process "cd ex1_prove/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  8:58:05 [ex1_prove] base: [INF:CM0023] Creating log file slpp_all/surelog.log.
SBY  8:58:05 [ex1_prove] base: [WRN:PA0205] ex1.sv:1:1: No timescale set for "ex1".
SBY  8:58:05 [ex1_prove] base: [INF:CP0300] Compilation...
SBY  8:58:05 [ex1_prove] base: [INF:CP0303] ex1.sv:1:1: Compile module "work@ex1".
SBY  8:58:05 [ex1_prove] base: [INF:CP0302] Compile class "work@mailbox".
SBY  8:58:05 [ex1_prove] base: [INF:CP0302] Compile class "work@process".
SBY  8:58:05 [ex1_prove] base: [INF:CP0302] Compile class "work@semaphore".
SBY  8:58:05 [ex1_prove] base: [INF:EL0526] Design Elaboration...
SBY  8:58:05 [ex1_prove] base: [NTE:EL0503] ex1.sv:1:1: Top level module "work@ex1".
SBY  8:58:05 [ex1_prove] base: [NTE:EL0508] Nb Top level modules: 1.
SBY  8:58:05 [ex1_prove] base: [NTE:EL0509] Max instance depth: 1.
SBY  8:58:05 [ex1_prove] base: [NTE:EL0510] Nb instances: 1.
SBY  8:58:05 [ex1_prove] base: [NTE:EL0511] Nb leaf instances: 1.
SBY  8:58:05 [ex1_prove] base: [INF:UH0706] Creating UHDM Model...
SBY  8:58:05 [ex1_prove] base: [  FATAL] : 0
SBY  8:58:05 [ex1_prove] base: [ SYNTAX] : 0
SBY  8:58:05 [ex1_prove] base: [  ERROR] : 0
SBY  8:58:05 [ex1_prove] base: [WARNING] : 1
SBY  8:58:05 [ex1_prove] base: [   NOTE] : 5
SBY  8:58:05 [ex1_prove] base: Warning: ex1.sv:7: Skipping non-synthesizable object of type 'immediate_cover'
SBY  8:58:05 [ex1_prove] base: Warning: ex1.sv:8: Skipping non-synthesizable object of type 'immediate_cover'
SBY  8:58:05 [ex1_prove] base: finished (returncode=0)
SBY  8:58:05 [ex1_prove] smt2: starting process "cd ex1_prove/model; yosys -ql design_smt2.log design_smt2.ys"
SBY  8:58:05 [ex1_prove] smt2: finished (returncode=0)
SBY  8:58:05 [ex1_prove] engine_0.basecase: starting process "cd ex1_prove; yosys-smtbmc --presat --unroll --noprogress -t 2  --append 1 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY  8:58:05 [ex1_prove] engine_0.induction: starting process "cd ex1_prove; yosys-smtbmc --presat --unroll -i --noprogress -t 2  --append 1 --dump-vcd engine_0/trace_induct.vcd --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2"
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Solver: yices
SBY  8:58:05 [ex1_prove] engine_0.induction: ##   0:00:00  Solver: yices
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Checking assumptions in step 0..
SBY  8:58:05 [ex1_prove] engine_0.induction: ##   0:00:00  Trying induction in step 2..
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Checking assertions in step 0..
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  BMC failed!
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Appending additional step 1.
SBY  8:58:05 [ex1_prove] engine_0.induction: ##   0:00:00  Trying induction in step 1..
SBY  8:58:05 [ex1_prove] engine_0.induction: ##   0:00:00  Temporal induction successful.
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Re-solving with appended steps..
SBY  8:58:05 [ex1_prove] engine_0.induction: ##   0:00:00  Status: passed
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Assert failed in ex1: assert_a_neq_b
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY  8:58:05 [ex1_prove] engine_0.basecase: ##   0:00:00  Status: failed
SBY  8:58:05 [ex1_prove] engine_0.induction: finished (returncode=0)
SBY  8:58:05 [ex1_prove] engine_0: Status returned by engine for induction: pass
SBY  8:58:05 [ex1_prove] engine_0.basecase: finished (returncode=1)
SBY  8:58:05 [ex1_prove] engine_0: Status returned by engine for basecase: FAIL
SBY  8:58:05 [ex1_prove] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:58:05 [ex1_prove] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:58:05 [ex1_prove] summary: engine_0 (smtbmc) returned pass for induction
SBY  8:58:05 [ex1_prove] summary: engine_0 (smtbmc) returned FAIL for basecase
SBY  8:58:05 [ex1_prove] summary: counterexample trace: ex1_prove/engine_0/trace.vcd
SBY  8:58:05 [ex1_prove] DONE (FAIL, rc=2)
SBY  8:58:05 [ex1_cover] engine_0: smtbmc
SBY  8:58:05 [ex1_cover] base: starting process "cd ex1_cover/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  8:58:05 [ex1_cover] base: [INF:CM0023] Creating log file slpp_all/surelog.log.
SBY  8:58:05 [ex1_cover] base: [WRN:PA0205] ex1.sv:1:1: No timescale set for "ex1".
SBY  8:58:05 [ex1_cover] base: [INF:CP0300] Compilation...
SBY  8:58:05 [ex1_cover] base: [INF:CP0303] ex1.sv:1:1: Compile module "work@ex1".
SBY  8:58:05 [ex1_cover] base: [INF:CP0302] Compile class "work@mailbox".
SBY  8:58:05 [ex1_cover] base: [INF:CP0302] Compile class "work@process".
SBY  8:58:05 [ex1_cover] base: [INF:CP0302] Compile class "work@semaphore".
SBY  8:58:05 [ex1_cover] base: [INF:EL0526] Design Elaboration...
SBY  8:58:05 [ex1_cover] base: [NTE:EL0503] ex1.sv:1:1: Top level module "work@ex1".
SBY  8:58:05 [ex1_cover] base: [NTE:EL0508] Nb Top level modules: 1.
SBY  8:58:05 [ex1_cover] base: [NTE:EL0509] Max instance depth: 1.
SBY  8:58:05 [ex1_cover] base: [NTE:EL0510] Nb instances: 1.
SBY  8:58:05 [ex1_cover] base: [NTE:EL0511] Nb leaf instances: 1.
SBY  8:58:05 [ex1_cover] base: [INF:UH0706] Creating UHDM Model...
SBY  8:58:05 [ex1_cover] base: [  FATAL] : 0
SBY  8:58:05 [ex1_cover] base: [ SYNTAX] : 0
SBY  8:58:05 [ex1_cover] base: [  ERROR] : 0
SBY  8:58:05 [ex1_cover] base: [WARNING] : 1
SBY  8:58:05 [ex1_cover] base: [   NOTE] : 5
SBY  8:58:05 [ex1_cover] base: Warning: ex1.sv:7: Skipping non-synthesizable object of type 'immediate_cover'
SBY  8:58:05 [ex1_cover] base: Warning: ex1.sv:8: Skipping non-synthesizable object of type 'immediate_cover'
SBY  8:58:05 [ex1_cover] base: finished (returncode=0)
SBY  8:58:05 [ex1_cover] smt2: starting process "cd ex1_cover/model; yosys -ql design_smt2.log design_smt2.ys"
SBY  8:58:05 [ex1_cover] smt2: finished (returncode=0)
SBY  8:58:05 [ex1_cover] engine_0: starting process "cd ex1_cover; yosys-smtbmc --presat --unroll -c --noprogress -t 2  --append 1 --dump-vcd engine_0/trace%.vcd --dump-vlogtb engine_0/trace%_tb.v --dump-smtc engine_0/trace%.smtc model/design_smt2.smt2"
SBY  8:58:05 [ex1_cover] engine_0: ##   0:00:00  Solver: yices
SBY  8:58:05 [ex1_cover] engine_0: ##   0:00:00  Status: passed
SBY  8:58:05 [ex1_cover] engine_0: finished (returncode=0)
SBY  8:58:05 [ex1_cover] engine_0: Status returned by engine: pass
SBY  8:58:05 [ex1_cover] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:58:05 [ex1_cover] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  8:58:05 [ex1_cover] summary: engine_0 (smtbmc) returned pass
SBY  8:58:05 [ex1_cover] DONE (PASS, rc=0)
SBY  8:58:05 The following tasks failed: ['bmc', 'prove']

This actually fairs better than my real example, in that it actually runs the asserts. Covers are stripped as non synthesisisable. In reality, I instantiate a module within the design which contains the assumptions and assertions for the rules to apply for each port, as either a master or slave. I see warnings like

SBY  9:05:50 [dataflow_id_cover] base: Warning: Removing unused module: \dataflow_formal from the design.

I guess its stripped as all the ports are inputs. Is there a pragma to stop it stripping these, or a way when in formal mode to assume that code full of asserts / assumes is not unused?

alaindargelas commented 1 year ago

I made a fix in Surelog https://github.com/chipsalliance/Surelog/pull/3352 that will accept the -formal option and let the cover keyword be allowed in a "formal" category of keywords: synthesizable + formal. @rkapuscik please update uhdmastfrontend.cc: In member function 'virtual Yosys::AST::AstNode Yosys::UhdmAstFrontend::parse(std::string)': 02:42:28 | uhdmastfrontend.cc:47:120: error: no matching function for call to 'UHDM::SynthSubset::SynthSubset(UHDM::Serializer, std::set<const UHDM::BaseClass>&, bool)' 02:42:28 | 47 | UHDM::SynthSubset synthSubset = new UHDM::SynthSubset(&serializer, this->shared.nonSynthesizableObjects, false); 02:42:28 | | ^ 02:42:28 | In file included from uhdmcommonfrontend.h:23, 02:42:28 | from uhdmastfrontend.cc:20: 02:42:28 | /root/Surelog/Surelog/yosys-uhdm-plugin-integration/image/include/uhdm/SynthSubset.h:39:3: note: candidate: 'UHDM::SynthSubset::SynthSubset(UHDM::Serializer, std::set<const UHDM::BaseClass>&, bool, bool)' 02:42:28 | 39 | SynthSubset(Serializer* serializer, 02:42:28 | | ^~~ https://github.com/chipsalliance/Surelog/actions/runs/3519786113/jobs/5900084759

ollie-etl commented 1 year ago

@alaindargelas Thanks for looking into this.

Isweet commented 6 months ago

We're also interested in using SynLig for parsing assume property and assert property statements in SystemVerilog. Is that currently possible?

I've tried a simple example with read_systemverilog -formal -defer, and it seems to complain about them as non-synthesizable and ignore them.

alaindargelas commented 6 months ago

The whole formal verification support in read_systemverilog is not going to get any attention until properly funded by someone. A workaround, of course is to move those statements in files that can be read by read_verilog and read the rest of the design with read_systemverilog

chipsalliance / synlig

read_systemverilog `-formal` support #1248