P2: Circuit Equivalence Checking

You will implement a Jupyter notebook which can check for the behavioral equivalence of arbitrary combinatorial circuit designs expressed in the Verilog hardware description language.

Setup

Install Clingo: https://github.com/potassco/clingo/releases Links to an external site.

Install Yosys (you can earn 7 points before a step that requires this to be installed): http://www.clifford.at/yosys/ Links to an external site. Links to an external site.

Download assignment support files from Canvas: 

- adders-3.lp Download adders-3.lp

- adders-3.json Download adders-3.json

- adders-3.v Download adders-3.v

- adders.v Download adders.v

- mycells.lib Download mycells.lib

Grading Criteria / Suggested Work Plan

[5pts] Symbolic simulation: Create a symbolic simulation of the two devices described in adders-3.lp. It describes two different 3-bit adder designs, but one design has a bug. You will create a new program called sim.lp such that when you run the command “clingo sim.lp adders-3.lp”, the one solution found witnesses an input on which the two circuits disagree. The solution will take the form of a choice of how to set the 0/1 value of each of the bits on each of the input ports. Your sim.lp file and the command that runs it should be embedded in your notebook. Here's an example of using ASP from inside of a notebook: https://gist.github.com/rndmcnlly/5f9d60280f9c825666963022c7d530dc Links to an external site.

[1pt] Output wrangling: Use the “--outf=2” command line flag for clingo to capture the output of the solver in a form you can parse. Wrangle that output to cleanly extract the critical input values (a and b) and show the different output values (out) that they yield.

[1pt] Input wrangling: Wrangle the circuit descriptions in a JSON file into a set of logical facts. You should write some Python code to transform adders-3.json into a file adders.lp that is equivalent to adders-3.lp.

[1pt] Circuit synthesis: Use the Yosys logic synthesis tool to transform the circuit design in adders.v into adders.json. Unlike the “-3” files, this describes 32-bit adders (which have the same bug as the small ones). Although it only takes one command line call to yosys to do the synthesis, you also need to specify a gate library (mycells.lib).

[1pt] Integration: Put all of these together in one big notebook that shows how to find the critical input for which the two 32-bit adder designs disagree. That is, it should start with Verilog file and not rely on any of the “-3” files.

[1pt] Generalization: Refine the notebook so that it doesn’t assume the one specific bug you found in the adder designs previously. If you changed the input designs to be the same, the running the notebook should report that the designs are equivalent. It’s okay to assume that both circuits have same-sized inputs called a, b and an output called out, but don’t assume they are trying to implement addition or that they disagree exactly once -- they could disagree zero times or zillions of times.

Outline of final notebook (with clues for each step)

• Embed the behavioral circuit descriptions (adders.v) file in the notebook. (Use the %%file cell magic).
• Embed the gate library (mycells.lib) file in the notebook.
• Use yosys to synthesize a gate-level model of the circuits, producing a JSON result file.
  • yosys \
    -p "synth; abc -liberty mycells.lib; clean; write_json adders.json" \
    -QT -f verilog adders.v
• Wrangle the JSON files into a bunch of AnsProlog facts like in adders-3.lp. In the gate descriptions, the last wire number mentioned is always the output of the gate.
• Create a symbolic circuit simulator (sim.lp)
  • Suggested predicates to define in your program:
    • input_port(Port)
      input_port_width(Port,Width)
      output_port(Port)
      common_input_signal(Port,Bit,Value)
      signal(Device,Wire,Value)
      output_signal(Device,Port,Bit,Value)
      disagreement
  • Suggested development steps:
    • Use normal rules to define input_port/1, input_port_width/2, and output_port/1 in terms of the device_ facts previously generated.
    • If you run “clingo sim.lp adders-3.lp --text”, you should see your rules doing the right thing.
    • Use this choice rule with nondeterministically guess one value for each bit of each input port:
      
      • 1 { common_input_signal(P,B,0..1) } 1 :- input_port_width(P,W); B=0..W-1.
        
    • If you run clingo with the extra argument “0” (and no “--text”) to list all possible solutions, you should find 64 solutions. (2^6=64)
    • Use a normal rule to copy the chosen common input signals to the wires inside of each adder. This rule will have signal(Dev,Wire,Val) in the head and reference common_input_signal/3 and device_port_bit_wire/4 in the body.
    • At this point, you should comment out that choice rule and instead hard-code 6 facts (maybe setting all input bits to 0) for testing purposes.
    • Using several normal rules, define the signal value for wires on the output of logic gates based on the signal value for the inputs. The device_gate/3 predicate describes which wires are connected by what kind of gate. Here’s the implementation of or_gate (you should support and_gate and not_gate):
      • signal(D,OutWire,1-(1-VA)*(1-VB)) :-
            device_gate(D,or_gate,(AWire,BWire,OutWire));
            signal(D,AWire,VA);
            signal(D,BWire,VB).
    • f you have hard-coded test inputs, you can again use “--text” to see if the rules you wrote are behaving the way you expect.
      
    • Using one last normal rule, define disagreement/0 by checking if there is some port P and bit index B for which devices D1 and D2 (D1 != D2) yield values V1 and V2 where V1 != V2.
      
    • On the test inputs, there should be no disagreement. If you replace the test inputs with the choice rule again, there should still only be 64 solutions, but one of them will witness disagreement.
      
    • Using one integrity constraint, reject models where there is no disagreement:
      • :- not disagreement.
    • Now when you ask for all models, there should be exactly 1.
• Run clingo on sim.lp and adders.lp together to find one solution (a counterexample to the claim that the circuits are equivalent).
• Run clingo with “--outf=2” to get some JSON output you can parse to extract the critical inputs in a human-readable form (e.g. “a=6; b=3” rather than a list of bit values).