Check if two combinatorial circuits defined in Verilog are behaviorally equivalent (synthesis to a sea of gates using Yosys and search using Potassco)

Equivalence.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "# Overview\n",
    "\n",
    "Let's find try to prove that two different circuit designs have equivalent input/output behavior (or find an input for which their outputs disagree).\n",
    "\n",
    "We'll start with two circuit designs expressed in Verilog. We'll use the Yosys  logic synthesis tool (http://www.clifford.at/yosys/) to convert them into a graph of logic gates. Then we'll use ASP to symbolically reason about the circuit behavior, searching for a case where the designs disagree."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "# Adder Designs in Verilog\n",
    "The first design (`good_adder`) does the obvious thing.\n",
    "The second design (`bad_adder`) falls apart in rare occasions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Overwriting adders.v\n"
     ]
    }
   ],
   "source": [
    "%%file adders.v\n",
    "\n",
    "module good_adder(a, b, out);\n",
    "    parameter WIDTH = 32;\n",
    "    input [WIDTH-1:0] a;\n",
    "    input [WIDTH-1:0] b; \n",
    "    output [WIDTH-1:0] out;\n",
    "    \n",
    "    assign out = a + b;\n",
    "endmodule\n",
    "\n",
    "module bad_adder(a, b, out);\n",
    "    parameter WIDTH = 32;\n",
    "    input [WIDTH-1:0] a;\n",
    "    input [WIDTH-1:0] b; \n",
    "    output [WIDTH-1:0] out;\n",
    "\n",
    "    assign out = (a == 'd6 && b == 'd3) ? 10 : a + b;\n",
    "endmodule"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "# Cell library\n",
    "In a real hardware design scenario, we'd ask the synthesis tool to target whatever primitive devices were supported by the target platform. This is a toy problem, so let's just define some simple and familiar building blocks."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Overwriting mycells.lib\n"
     ]
    }
   ],
   "source": [
    "%%file mycells.lib\n",
    "\n",
    "library(demo) {\n",
    "    cell(BUF) {\n",
    "        area: 6;\n",
    "        pin(A) { direction: input; }\n",
    "        pin(Y) { direction: output; function: \"A\"; }\n",
    "    }\n",
    "    cell(NOT) {\n",
    "        area: 3;\n",
    "        pin(A) { direction: input; }\n",
    "        pin(Y) { direction: output; function: \"A'\"; }\n",
    "    }\n",
    "    cell(AND) {\n",
    "        area: 4;\n",
    "        pin(A) { direction: input; }\n",
    "        pin(B) { direction: input; }\n",
    "        pin(Y) { direction: output; function: \"A*B\"; }\n",
    "    }\n",
    "    cell(OR) {\n",
    "        area: 4;\n",
    "        pin(A) { direction: input; }\n",
    "        pin(B) { direction: input; }\n",
    "        pin(Y) { direction: output; function: \"A+B\"; }\n",
    "    }\n",
    "    cell(DFF) {\n",
    "        area: 18;\n",
    "        ff(IQ, IQN) { clocked_on: C; next_state: D; }\n",
    "        pin(C) { direction: input; clock: true; }\n",
    "        pin(D) { direction: input; }\n",
    "        pin(Q) { direction: output; function: \"IQ\"; }\n",
    "    }\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "# Synthesis\n",
    "Let's turn those adders into a graph of logic gates using Yosys."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true,
    "scrolled": false
   },
   "outputs": [],
   "source": [
    "!yosys -q \\\n",
    "    -p \"synth; abc -liberty mycells.lib; clean; write_json adders.json\" \\\n",
    "    -f verilog adders.v"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "# Wrangling: JSON-to-LP\n",
    "The output from Yosys has a lot of information. Let's find the important parts (the set of primitive devices within each adder design)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true,
    "scrolled": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "{\r\n",
      "  \"creator\": \"Yosys 0.7 (git sha1 UNKNOWN, clang 8.0.0 -fPIC -Os)\",\r\n",
      "  \"modules\": {\r\n",
      "    \"bad_adder\": {\r\n",
      "      \"attributes\": {\r\n",
      "        \"src\": \"adders.v:11\"\r\n",
      "      },\r\n",
      "      \"ports\": {\r\n",
      "        \"a\": {\r\n",
      "          \"direction\": \"input\",\r\n"
     ]
    }
   ],
   "source": [
    "!head adders.json"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true,
    "scrolled": false
   },
   "outputs": [],
   "source": [
    "import json\n",
    "with open(\"adders.json\") as f:\n",
    "    yosys_result = json.load(f)\n",
    "\n",
    "with open(\"adders.lp\", \"w\") as f:\n",
    "    for module_name, module in yosys_result['modules'].items():\n",
    "        f.write(\"device(%s).\\n\" % module_name)\n",
    "        for port_name, port in module['ports'].items():\n",
    "            f.write(\"device_port_direction(%s,%s,%s).\\n\" % (module_name, port_name, port['direction']))\n",
    "            f.write(\"device_port_width(%s,%s,%d).\\n\" % (module_name, port_name, len(port['bits'])))\n",
    "            for i,bit in enumerate(port['bits']):\n",
    "                f.write(\"device_port_bit_wire(%s,%s,%d,%d).\\n\" % (module_name, port_name, i, bit))\n",
    "        for cell_name, cell in module['cells'].items():\n",
    "            cell_type = cell['type'].lower()\n",
    "            # Beware: \"not\" is a keyword in AnsProlog\n",
    "            assert cell_type in ['and', 'or', 'not']\n",
    "            connections = tuple([c[1][0] for c in sorted(cell['connections'].items())])\n",
    "            f.write(\"device_gate(%s,%s_gate,%s).\\n\" % (module_name, cell_type, str(connections)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "device(good_adder).\r\n",
      "device_port_direction(good_adder,a,input).\r\n",
      "device_port_width(good_adder,a,32).\r\n",
      "device_port_bit_wire(good_adder,a,0,2).\r\n",
      "device_port_bit_wire(good_adder,a,1,3).\r\n",
      "device_port_bit_wire(good_adder,a,2,4).\r\n",
      "device_port_bit_wire(good_adder,a,3,5).\r\n",
      "device_port_bit_wire(good_adder,a,4,6).\r\n",
      "device_port_bit_wire(good_adder,a,5,7).\r\n",
      "device_port_bit_wire(good_adder,a,6,8).\r\n"
     ]
    }
   ],
   "source": [
    "!head adders.lp"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "# Symbolic Simulation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Overwriting sim.lp\n"
     ]
    }
   ],
   "source": [
    "%%file sim.lp\n",
    "\n",
    "input_port(P) :- device_port_direction(D,P,input).\n",
    "input_port_width(P,W) :- input_port(P); device_port_width(D,P,W).\n",
    "output_port(P) :- device_port_direction(D,P,output).\n",
    "\n",
    "1 { common_input_signal(P,B,0..1) } 1 :- input_port_width(P,W); B=0..W-1.\n",
    "    \n",
    "signal(D,Wire,V) :- common_input_signal(P,B,V); device_port_bit_wire(D,P,B,Wire).\n",
    "    \n",
    "signal(D,OutWire,1-V) :-\n",
    "    device_gate(D,not_gate,(InWire,OutWire));\n",
    "    signal(D,InWire,V).\n",
    "    \n",
    "signal(D,OutWire,VA*VB) :-\n",
    "    device_gate(D,and_gate,(AWire,BWire,OutWire));\n",
    "    signal(D,AWire,VA);\n",
    "    signal(D,BWire,VB).\n",
    "\n",
    "signal(D,OutWire,1-(1-VA)*(1-VB)) :-\n",
    "    device_gate(D,or_gate,(AWire,BWire,OutWire));\n",
    "    signal(D,AWire,VA);\n",
    "    signal(D,BWire,VB).\n",
    "\n",
    "output_signal(D,P,B,V) :-\n",
    "    output_port(P);\n",
    "    device_port_bit_wire(D,P,B,Wire);\n",
    "    signal(D,Wire,V).\n",
    "    \n",
    "disagreement :-\n",
    "    output_signal(D1,P,B,V1);\n",
    "    output_signal(D2,P,B,V2);\n",
    "    D1 != D2;\n",
    "    V1 != V2.\n",
    "   \n",
    ":- not disagreement.\n",
    "\n",
    "#show common_input_signal/3.\n",
    "#show output_signal/4."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "Let's search for disagreements:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true,
    "scrolled": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "clingo version 5.1.0\n",
      "Reading from sim.lp ...\n",
      "Solving...\n",
      "SATISFIABLE\n",
      "\n",
      "Models       : 1+\n",
      "Calls        : 1\n",
      "Time         : 0.173s (Solving: 0.12s 1st Model: 0.12s Unsat: 0.00s)\n",
      "CPU Time     : 0.170s\n"
     ]
    }
   ],
   "source": [
    "!clingo sim.lp adders.lp -q"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "There's at least one counterexample to the claim that the circuits are equivalent. Let's wrangle the output of clingo to recover the values in a more readable form."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[('a', 6), ('b', 3), ('bad_adder_out', 10), ('good_adder_out', 9)]\n"
     ]
    }
   ],
   "source": [
    "lines = !clingo sim.lp adders.lp --outf=2\n",
    "result = json.loads(\"\\n\".join(lines))\n",
    "facts = result['Call'][0]['Witnesses'][0]['Value']\n",
    "\n",
    "from collections import defaultdict\n",
    "\n",
    "values = defaultdict(lambda: 0)\n",
    "\n",
    "def common_input_signal(port, bit, weight):\n",
    "    values[port] += (1<<bit)*weight\n",
    "    \n",
    "def output_signal(device, port, bit, weight):\n",
    "    name = \"%s_%s\" % (device, port)\n",
    "    values[name] += (1<<bit)*weight\n",
    "\n",
    "for f in facts:\n",
    "    eval(f,{\n",
    "        'a': 'a',\n",
    "        'b': 'b',\n",
    "        'out': 'out',\n",
    "        'good_adder': 'good_adder',\n",
    "        'bad_adder': 'bad_adder',\n",
    "        'common_input_signal': common_input_signal,\n",
    "        'output_signal': output_signal})\n",
    "\n",
    "print sorted(values.items())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "Those numbers look familiar!\n",
    "\n",
    "In the end the adders weren't equivalent. Of the 18 quintillion possile inputs, now we know at least one concrete input on which they disagree."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "# High-level Simulation\n",
    "Let's use Yosys to plug these values back into the original high-level circuit description and simulate it without turning it into a sea of logic gates first."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Eval result: \\gate_out = 10.\r\n",
      "Eval result: \\gold_out = 9.\r\n",
      "Eval result: \\trigger = 1'1.\r\n"
     ]
    }
   ],
   "source": [
    "!yosys -p 'miter -equiv -make_outputs -flatten good_adder bad_adder miter' \\\n",
    "       -p 'select miter; eval -set in_a 6 -set in_b 3' \\\n",
    "       -f verilog -QT adders.v | tail -n 3"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "deletable": true,
    "editable": true
   },
   "source": [
    "Yosys can even search for these critical input values by itself using an internal SAT solver."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {
    "collapsed": false,
    "deletable": true,
    "editable": true,
    "scrolled": false
   },
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Solving problem with 1045 variables and 2829 clauses..\r\n",
      "SAT proof finished - model found: FAIL!\r\n",
      "\r\n",
      "   ______                   ___       ___       _ _            _ _ \r\n",
      "  (_____ \\                 / __)     / __)     (_) |          | | |\r\n",
      "   _____) )___ ___   ___ _| |__    _| |__ _____ _| | _____  __| | |\r\n",
      "  |  ____/ ___) _ \\ / _ (_   __)  (_   __|____ | | || ___ |/ _  |_|\r\n",
      "  | |   | |  | |_| | |_| || |       | |  / ___ | | || ____( (_| |_ \r\n",
      "  |_|   |_|   \\___/ \\___/ |_|       |_|  \\_____|_|\\_)_____)\\____|_|\r\n",
      "\r\n",
      "\r\n",
      "  Signal Name             Dec       Hex                                 Bin\r\n",
      "  --------------- ----------- --------- -----------------------------------\r\n",
      "  \\gate_out                10         a    00000000000000000000000000001010\r\n",
      "  \\gold_out                 9         9    00000000000000000000000000001001\r\n",
      "  \\in_a                     6         6    00000000000000000000000000000110\r\n",
      "  \\in_b                     3         3    00000000000000000000000000000011\r\n",
      "  \\trigger                  1         1                                   1\r\n"
     ]
    }
   ],
   "source": [
    "!yosys -p 'miter -equiv -make_assert -make_outputs -flatten good_adder bad_adder miter' \\\n",
    "       -p 'sat -show-inputs -show-outputs -prove-asserts miter' \\\n",
    "       -f verilog -QT adders.v | tail -n 18"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 2",
   "language": "python",
   "name": "python2"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 2
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython2",
   "version": "2.7.12"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}