Bluecheck with imported Verilog

[podhrmic]

Hello!
I have a Bluespec project (a simple SoC) with imported Verilog files. My understanding is that I cannot use Bluecheck to test properties for such design - is that correct? I currently elaborate everything into verilog with bsc -u -elab -verilog ... and then use Verilator for simulation.

Perhaps there is a way to treat the Verilog imports (import "BVI" ...) as blackboxes, and still test properties for the remaining pure Bluespec code?

[quark17]

I don't see why imported Verilog should be a problem for Bluecheck. I assume you're referring to this project which is separate from BSC?

The Bluecheck infrastructure instantiates a design and a golden model, and it interacts with them only through the top interface (I believe). I don't think it should matter whether the design has any imported Verilog (and in fact the entire design could be imported Verilog). Also, if your golden model is synthesizable, then the whole thing can even be synthesized and run, say, in an FPGA.