search

SpinalHDL / SpinalHDL

Scala based HDL
Other
1.68k stars 332 forks source link

Reset handling and formal statements #471

Open piegamesde opened 3 years ago

piegamesde commented 3 years ago

Kind of a sub-thread of #137 specific to resets.

At the moment, all statements are generated implicitly inside a block that only runs when the system is running. This kind of makes sense when writing hardware in general, but formal verification needs to also verify the reset handling itself so this doesn't work. This is a huge foot gun because proofs will pass although the statements where never active.

The current solution is to wrap all formal statements in ClockDomain.current.withoutReset() {…}, but this is overly verbose and hard to discover. I think it would be better to make this the default for GenerationFlags.formal {…} and also to document this. Also, maybe it is possible to emit a warning then somebody writes a broken when clockDomain.isResetActive {…}.

Dolu1990 commented 3 years ago

Hi,

About reset handling, the 1.6.0 added a few feature which could allow writing formal stuff differently. I just documented them : https://github.com/SpinalHDL/SpinalDoc-RTD/commit/9b8a7378e4db9a41a5319cda4c3a70f1281db63c

I'm not personnaly using formal, so i can't assert myself about how much it can be used.

If you give a try, let's me know :)

Also, i suspect we could now avoid this initstate (https://github.com/SpinalHDL/SpinalDoc-RTD/commit/9b8a7378e4db9a41a5319cda4c3a70f1281db63c#diff-3531283ef5ff0b30072a58ca4193283e83c7df758c657a6e0e6595566f6440d1R31)

And maybe have something more robust with those additions ?

Readon commented 1 year ago

@piegamesde could you provide some minimal example code which could be tested?