← portfolio  /  HW emulation
Compiler · Runtime · FPGA

RTL Emulation Platform

Simulation versus emulation: simulation evaluates an RTL model entirely in software, while emulation executes compiled RTL on accelerated hardware for faster testing and hardware-software verification.

Formal verification

Model checking example

Download files
01 · Passing proof

Request / grant controller

A simple FSM: idle → queued → granting.

RTL · request_grant_fsm.sv 
Loading…
Property · request_grant_properties.sv 
Loading…
Property as LTL 
G(busy <-> !ready)
G(grant -> (busy && !ready))
G((request && ready) -> F(grant))
1 · Frontend elaborated-design dump 
Loading…
2 · BTOR2 HIR, unoptimized 
Loading…
3 · BTOR2 HIR, optimized 
Loading…
4 · Low BTOR2, unoptimized 
Loading…
5 · Low BTOR2, optimized 
Loading…
6 · Proof result 
Loading…
02 · Injected failure

Counterexample and witness

INJECT_FAULT advertises controller availability even when it is busy processing the previous request.

Counterexample waveform
clkrst_nrequeststatefault cycle 0cycle 1 10 · granting ready=1 · busy=1 · grant=1 → safety violation
Counterexample result 
Loading…
Decoded witness 
Loading…
Counterexample VCD 
Loading…
Formal flow

Current limitations

Limitations

Current limitations

Examples

Download files
01 · Adder

Host-controlled inputs

adder_tb.sv 
Loading…
adder.sv 
Loading…
program.eir · FPGA IR 
Loading…
program.vir · host IR 
Loading…
program.disasm 
Loading…
02 · Circular buffer

Small UVM test

circular_buffer_uvm_pkg.sv 
Loading…
circular_buffer_uvm_tb.sv 
Loading…
circular_buffer.sv 
Loading…
program.eir · FPGA IR 
Loading…
program.vir · host IR 
Loading…
program.disasm 
Loading…
Demo