EBMC – Verilog Language Features

Synthesizable Subset of Verilog

EBMC supports most of those parts of the IEEE 1800-2017 SystemVerilog standard that are commonly considered "synthesizable".

Construct	Keywords	Notes	Supported?
ports	input, output, inout	Use inout port only at IO level	✔
parameters	parameter	Allows more generic design style	✔
module definition	module	Used to define Verilog module structure	✔
signals and variables	wire, reg, tri	different signal types, allows vector type	✔
instantiation	module instance/primitive gate level instances	Used to instantiate one module inside another	✔
function and tasks	function, task	reduces repeated code, doesnot allow timing	✔
procedural constructs	always, if, else, case, casex, casez	synthesizable set except initial block	✔
procedural block	begin, end, named blocks, disable	Allows disabling of named blocks	✔
procedural assignments	blocking, non-blocking	allows assignments to registers in blocking or non-blocking fashion	✔
Assignment	assign	continuous assignment to wires in combinatorial block	✔
loops	for, while, forever	looping constructs used in Verilog	✔
named blocks	disable	Supports disabling of named blocks	✘

Non-synthesizable Subset of Verilog

EBMC gives verification semantics to some parts of the IEEE 1800-2017 SystemVerilog standard that are not commonly considered "synthesizable".

Construct	Keywords	Notes	Supported?
	initial	Used only in test benches	✔
events		Used in test benches for syncing test bench components	✘
	real	Real data type not supported	✘
	force, release	Force and Release data-types not supported	✘
	assign, deassign	assign and deassign on reg type data not supported, but assign supported on wire data type	✔
	fork, join	Not supported. Can be simulated using nonblocking assignments	✘
primitives		only gate level primitives supported	✔
UDP and tables			✘