search

YosysHQ / yosys

Yosys Open SYnthesis Suite
https://yosyshq.net/yosys/
ISC License
3.49k stars 890 forks source link

Segmentation fault with verific #4102

Open CrazybinaryLi opened 10 months ago

CrazybinaryLi commented 10 months ago

Version

Yosys 0.36 (git sha1 8f07a0d84, clang 10.0.0-4ubuntu1 -fPIC -Os)

On which OS did this happen?

Linux

Reproduction Steps

I am using tabby with the yosys -verific command under a licensed application to read files in this repository (https://github.com/upscale-project/generic-sqed-demo) and generate .btor2 files. However, I encountered a segmentation fault error. The yosys script (.ys) which be used as follows: verific -vlog-incdir ./ridecore-src-buggy/;

verific -sv \ ./ridecore-src-buggy/define.v \ ./ridecore-src-buggy/topsim.v \ ./ridecore-src-buggy/alloc_issue_ino.v \ ./ridecore-src-buggy/search_be.v \ ./ridecore-src-buggy/srcsel.v \ ./ridecore-src-buggy/alu_ops.vh \ ./ridecore-src-buggy/arf.v \ ./ridecore-src-buggy/ram_sync.v \ ./ridecore-src-buggy/ram_sync_nolatch.v \ ./ridecore-src-buggy/brimm_gen.v \ ./ridecore-src-buggy/constants.vh \ ./ridecore-src-buggy/decoder.v \ ./ridecore-src-buggy/dmem.v \ ./ridecore-src-buggy/exunit_alu.v \ ./ridecore-src-buggy/exunit_branch.v \ ./ridecore-src-buggy/exunit_ldst.v \ ./ridecore-src-buggy/exunit_mul.v \ ./ridecore-src-buggy/imem.v \ ./ridecore-src-buggy/imm_gen.v \ ./ridecore-src-buggy/pipeline_if.v \ ./ridecore-src-buggy/gshare.v \ ./ridecore-src-buggy/pipeline.v \ ./ridecore-src-buggy/oldest_finder.v \ ./ridecore-src-buggy/btb.v \ ./ridecore-src-buggy/prioenc.v \ ./ridecore-src-buggy/mpft.v \ ./ridecore-src-buggy/reorderbuf.v \ ./ridecore-src-buggy/rrf_freelistmanager.v \ ./ridecore-src-buggy/rrf.v \ ./ridecore-src-buggy/rs_alu.v \ ./ridecore-src-buggy/rs_branch.v \ ./ridecore-src-buggy/rs_ldst.v \ ./ridecore-src-buggy/rs_mul.v \ ./ridecore-src-buggy/rs_reqgen.v \ ./ridecore-src-buggy/rv32_opcodes.vh \ ./ridecore-src-buggy/src_manager.v \ ./ridecore-src-buggy/srcopr_manager.v \ ./ridecore-src-buggy/storebuf.v \ ./ridecore-src-buggy/tag_generator.v \ ./ridecore-src-buggy/dualport_ram.v \ ./ridecore-src-buggy/alu.v \ ./ridecore-src-buggy/multiplier.v \ ./sqed-generator/SQED-Generator/QEDFiles/inst_constraints.v \ ./sqed-generator/SQED-Generator/QEDFiles/modify_instruction.v \ ./sqed-generator/SQED-Generator/QEDFiles/qed_decoder.v \ ./sqed-generator/SQED-Generator/QEDFiles/qed_i_cache.v \ ./sqed-generator/SQED-Generator/QEDFiles/qed_instruction_mux.v \ ./sqed-generator/SQED-Generator/QEDFiles/qed.v ;

prep -top topsim;

hierarchy -check;

chformal -assume -early;

memory;

flatten;

sim -clock clk -resetn reset_x -n 5 -rstlen 5 -zinit -w topsim;

setundef -undriven -expose;

write_btor fsm.btor2;

Expected Behavior

Produce the fsm.btor2 file

Actual Behavior

Segmentation fault (core dumped)

nakengelhardt commented 10 months ago

You have line breaks between the file names, which is an error: line break starts a new command. (The semicolons in your script are useless since they are not separating two commands on the same line.)

I can't reproduce a segfault, I get an error as expected: ERROR: Reading Verilog/SystemVerilog sources failed.

If I replace all line breaks with spaces in the script, it seems to work correctly, and I get the error VERIFIC-ERROR [VERI-1517] cannot open Verilog file './sqed-generator/SQED-Generator/QEDFiles/inst_constraints.v' - and there is indeed no such file.

CrazybinaryLi commented 10 months ago

Run the script ./setup-sqed-generator.sh to install the SQED generator (a git repository will be cloned from GitHub).

Run the script ./generate-qed-files.sh to generate the Verilog sources of the generic QED module for RIDECORE.

Run the script ./wire-up-qed-module.sh to wire up the QED module to the RIDECORE design and apply simplifications to speed up model checking.