Go beyond chosen traces
Tests exercise the sequences you run. A bounded check asks whether a violation exists across the allowed sequences in your model.
Explore a missed sequence ↑Firmware & RTL verification · Powered by CQ-SAT
Find the failure.
Keep the evidence.
Can your controller reach a bad state? Check a defined number of steps, replay a failure, or independently verify a bounded safety result.
A bounded checkModel + property + step limit
UNSAFE
Here is the sequence that breaks the property.
SAFE · bounded
No violation within the reviewed model and step limit.
REFUSED
The check cannot return a logical answer.
See what a failure looks like
One missed step can matter.
Choose a controller, play its trace, then switch on the corrected logic to see what changes.
Explore a failure sequence
Can motion continue after the guard opens?
A delayed interlock leaves the motor enabled for one step after the guard opens.
Illustrative four-step traces, not GCC runs. The corrected trace alone is not a proof.
Step 0: Guard closed. Motor enabled. Property holds at this step.
Click a step to inspect it
GCC asks whether any allowed sequence can violate the property within the bound. An UNSAFE witness gives you a concrete sequence to replay; a checked SAFE result covers the declared bounded model.
Why use GCC?
When a pass or fail is not enough.
Keep a reviewable evidence bundle
Bounded checking is established. GCC brings the model, assumptions, bound, result and independently checkable evidence into one governed workflow.
Inspect published evidence →Evaluate specialised solving
CQ-SAT targets suitable structure. A static gate selects it; other supported cases use an exact fallback. Measure suitability on your design.
Run an evaluation →A good fit: a specific firmware or RTL safety question, a reviewed model and a finite horizon. GCC complements testing; it does not promise universal speedups or unbounded verification.
How it works
Define. Check. Verify.
Define the question
Model + assumptions + bad state + step limit
Run an exact check
Eligible CQ-SAT route or supported exact fallback
Check the evidence
Independently verify a proof or replay a failure
Try a real evaluation
Use your design. Keep your RTL private.
Run the published workflow on your own ephemeral Linux worker. Return only a non-confidential outcome and suitability assessment.
Research prototype, release v0.32.0. Not certified or production-qualified. SAFE applies only to the reviewed model, assumptions, property and horizon. Review the production gaps.