QuestaSim vlog Compiler does not allow `assume` in Verilog files

[eldrickm]

Issue:

The generator outputs an inst_constraint.v file, a Verilog file with an assume property definition to constrain instructions to valid instructions only.

QuestaSim's vlog compiler seems to not allow assume in Verilog files. Error trace given below.:

========== Intializing Questa Workspace ==========
/cad/mentor/qformal/linux_x86_64/modeltech/plat/vlib work
/cad/mentor/qformal/linux_x86_64/modeltech/plat/vmap work work
QuestaSim-64 vmap 10.5c Lib Mapping Utility 2016.07 Jul 20 2016
vmap work work
Copying /hd/cad/mentor/qformal/share/modeltech/linux_x86_64/../modelsim.ini to modelsim.ini
Modifying modelsim.ini
mkdir -p output
========== Compiling Design ==========
./patches/patch.sh
/cad/mentor/qformal/linux_x86_64/modeltech/plat/vlog -f design/design.flist -f formal/formal.flist -l output/vlog.rpt
QuestaSim-64 vlog 10.5c Compiler 2016.07 Jul 20 2016
Start time: 11:24:48 on Mar 28,2021
vlog -f design/design.flist -f formal/formal.flist -l output/vlog.rpt
-- Compiling module alu
-- Compiling module branch_unit
-- Compiling module csr_file
-- Compiling module decoder
-- Compiling module design_top
-- Compiling module imm_generator
-- Compiling module integer_file
-- Compiling module load_unit
-- Compiling module machine_control
-- Compiling module ram
-- Compiling module steel_top
-- Compiling module store_unit
-- Compiling module inst_constraint
** Error: ./qed/inst_constraints.v(120): Checker 'assume' not found.  Instantiation 'property' must be of a visible checker.
** Error: ./qed/inst_constraints.v(120): A begin/end block was found with an empty body.  This is permitted in SystemVerilog, but not permitted in Verilog.  Please look for any stray semicolons.
-- Compiling module modify_instruction
-- Compiling module qed_decoder
-- Compiling module qed_i_cache
-- Compiling module qed_instruction_mux
-- Compiling module qed
-- Compiling module formal_spec
-- Compiling module formal_bind
End time: 11:24:48 on Mar 28,2021, Elapsed time: 0:00:00
Errors: 2, Warnings: 0
make: *** [design] Error 2

The particular errors are:

-- Compiling module inst_constraint
** Error: ./qed/inst_constraints.v(120): Checker 'assume' not found.  Instantiation 'property' must be of a visible checker.
** Error: ./qed/inst_constraints.v(120): A begin/end block was found with an empty body.  This is permitted in SystemVerilog, but not permitted in Verilog.  Please look for any stray semicolons.

Potential Fix

Simply changing the filetype to a System Verilog file allows compilation for QuestaSim vlog Compiler. mv inst_constraint.v inst_constraint.sv

[lonsing]

Related to issue https://github.com/upscale-project/sqed-generator/issues/5, Yosys seems to be more tolerant when handling inputs that contain non-Verilog or non-standard Verilog features.

In particular, Yosys supports a subset of SystemVerilog for formal verification, including assume, cf. http://www.clifford.at/papers/2016/yosys-synth-formal/slides.pdf

To resolve this issue (and also https://github.com/upscale-project/sqed-generator/issues/5), we could add an optional "strict mode" to the generator to output only standard Verilog.

I suggest to make that strict mode optional because we still want to use the features of Yosys of handling a subset of SystemVerilog.