mmaroti · HackerTrans

5 tahun yang laludiscuss

I think you need more assumptions. This satisfies your requirements:

X(0) = 0000, Y(a) = 0001, X(a) = 0011, Y(2a)= 0111.

mmaroti

5 tahun yang laludiscuss

This is blatantly false. People are using formal verification tools in hardware design, and they do work and they do compose. Here is a simple verilog code which accomplishes some of what he wants.

  module Blinker (
   input wire clock,
   output reg state
  );
  
  always @(posedge clock)
   state <= !state;
  
  `if FORMAL
  
  always @(posedge clock)
   assert ($past(state) != state);
  
  `endif
  
  endmodule
  
  module testbench (
   input wire clock,
   output wire state1,
   output wire state2
  );
  
  Blinker blinker1(clock, state1);
  Blinker blinker2(clock, state2);
  
  `if FORMAL
  
  # assume that they are different
  assume (state1 != state2);
  
  # then they stay different
  always @(posedge clock)
    assert (state1 != state2);
  
  `endif
  
  endmodule

Of course you NEED clock wires to the blinker. Composability comes from the use of assume and assert. You assume that your environment is behaving according to spec and you prove that you are also behaving to spec PROVIDED the environment working correctly. See https://symbiyosys.readthedocs.io/en/latest/index.html for more details.

Moral of the story: broken spec cannot be used, and I am saying this as a mathematician!

comments